Use different universe levels.

Fixes #1.
leanprover-community · Dec 1, 2021 · e46540e · e46540e
1 parent cfcabfe
commit e46540e
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Qq/Macro.lean b/Qq/Macro.lean
@@ -71,8 +71,8 @@ def addSyntaxDollar : Syntax → Syntax
     Syntax.ident info rawVal (addDollar val) preresolved
   | stx => panic! "addSyntaxDollar {stx}"
 
-def mkAbstractedLevelName (e : Expr) : MetaM Name :=
-  e.getAppFn.constName?.getD `udummy
+def mkAbstractedLevelName (e : Expr) : MetaM Name := do
+  e.getAppFn.constName?.getD `udummy ++ (← mkFreshId)
 
 def isBad (e : Expr) : Bool := do
   if let Expr.const (Name.str _ "rec" _) _ _ := e.getAppFn then