Solve conflict between do-mode and term-mode assumeInstancesCommute

leanprover-community · Jul 15, 2023 · c0d9516 · c0d9516
1 parent b7c3ebf
commit c0d9516
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git a/Qq/AssertInstancesCommute.lean b/Qq/AssertInstancesCommute.lean
@@ -2,7 +2,7 @@ import Qq.MetaM
 
 namespace Qq
 
-scoped syntax "assumeInstancesCommute" term : term
+scoped syntax "assumeInstancesCommute'" term : term
 
 namespace Impl
 open Lean Meta Elab Term
@@ -51,14 +51,14 @@ elab_rules : term <= expectedType | `(assertInstancesCommuteImpl $cont) => do
       expectedType
   | none => elabTerm cont expectedType
 
-elab_rules : term <= expectedType | `(assumeInstancesCommute $cont) => do
+elab_rules : term <= expectedType | `(assumeInstancesCommute' $cont) => do
   match ← findRedundantLocalInstQuoted? with
   | some ⟨fvar, _, _, lhs, rhs⟩ =>
     let n ← mkFreshUserName ((← fvar.getUserName).eraseMacroScopes.appendAfter "_eq")
     let ty := q(QE $lhs $rhs)
     elabTerm (← `(
         have $(mkIdent n) : $(← exprToSyntax ty) := ⟨⟩
-        assumeInstancesCommute $cont))
+        assumeInstancesCommute' $cont))
       expectedType
   | none => elabTerm cont expectedType
 
@@ -70,7 +70,7 @@ macro_rules
 syntax "assumeInstancesCommuteDummy" : term
 macro_rules
   | `(assert! assumeInstancesCommuteDummy; $cont) =>
-    `(assumeInstancesCommute $cont)
+    `(assumeInstancesCommute' $cont)
 
 end Impl
 open Impl

diff --git a/examples/strengthenInstance.lean b/examples/strengthenInstance.lean
@@ -19,5 +19,5 @@ def maybeReassocAlt {M : Q(Type $u)} (mul : Q(Mul $M)) (a b : Q($M)) :
 
 def maybeReassocPure {M : Q(Type $u)} (mul : Q(Mul $M)) (a b : Q($M)) (semigroup : Q(Semigroup $M)) :
     Q($a*($b*$b) = ($a*$b)*$b) :=
-  assumeInstancesCommute
+  assumeInstancesCommute'
   q(by rw [mul_assoc])