Fix #16

leanprover-community · Aug 18, 2024 · 338ce9d · 338ce9d
1 parent 71f5442
commit 338ce9d
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git a/Qq/Macro.lean b/Qq/Macro.lean
@@ -588,6 +588,7 @@ partial def floatExprAntiquot' [Monad m] [MonadQuotation m] (depth : Nat) :
   | `(q($x)) => do `(q($(← floatExprAntiquot' (depth + 1) x)))
   | `(Type $term) => do `(Type $(← floatLevelAntiquot' term))
   | `(Sort $term) => do `(Sort $(← floatLevelAntiquot' term))
+  | `($n:ident.{$us,*}) => do `($n.{$(← us.getElems.mapM floatLevelAntiquot'),*})
   | stx => do
     if let (some (kind, _pseudo), false) := (stx.antiquotKind?, stx.isEscapedAntiquot) then
       let term := stx.getAntiquotTerm

diff --git a/Qq/Match.lean b/Qq/Match.lean
@@ -400,6 +400,7 @@ private partial def floatExprAntiquot (depth : Nat) : Term → StateT (Array (TS
   | `(q($x)) => do `(q($(← floatExprAntiquot (depth + 1) x)))
   | `(Type $term) => do `(Type $(← floatLevelAntiquot term))
   | `(Sort $term) => do `(Sort $(← floatLevelAntiquot term))
+  | `($n:ident.{$us,*}) => do `($n.{$(← us.getElems.mapM floatLevelAntiquot),*})
   | stx => do
     if stx.1.isAntiquot && !stx.1.isEscapedAntiquot then
       let term : Term := ⟨stx.1.getAntiquotTerm⟩