Change guide syntax to 'using'

marcusrossel · Apr 12, 2024 · e78fe93 · e78fe93
1 parent d83ed78
commit e78fe93
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/Lean/Egg/Tactic/Guides.lean b/Lean/Egg/Tactic/Guides.lean
@@ -5,10 +5,10 @@ open Lean Elab Tactic
 namespace Egg.Guides
 
 declare_syntax_cat egg_guides
-syntax " via " (term,*) : egg_guides
+syntax &" using " (term,*) : egg_guides
 
 def parseGuides : TSyntax `egg_guides → TacticM Guides
-  | `(egg_guides|via $gs,*) => do
+  | `(egg_guides|using $gs,*) => do
     let mut guides : Guides := #[]
     for g in gs.getElems, idx in [:gs.getElems.size] do
       let guide ← Guide.from (← Tactic.elabTerm g none) (.guide idx)

diff --git a/Lean/Egg/Tests/Groups.lean b/Lean/Egg/Tests/Groups.lean
@@ -39,8 +39,8 @@ theorem inv_inv : -(-a) = a := by
        _ = _                := by group
 
 theorem neg_add' : -(a + b) = -b + -a := by
-  group via -b + -a + (a + b) + -(a + b)
+  group using -a + (a + b) + -(a + b)
 
 -- BUG: Try adding a hypothesis. This should cause the backend to crash.
 theorem inv_inv' : -(-a) = a := by
-  group via -(-a) + (-a + a)
+  group using (-a + a)