From 338ce9dd3aff55562c82387eff3caa79f0f8c333 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 18 Aug 2024 14:09:02 +0000
Subject: [PATCH] Fix #16

---
 Qq/Macro.lean | 1 +
 Qq/Match.lean | 1 +
 2 files changed, 2 insertions(+)

diff --git a/Qq/Macro.lean b/Qq/Macro.lean
index 070502a..51ac62a 100644
--- 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
index 0bc2798..806b63f 100644
--- 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⟩