use macro "constructor := fconstructor"

hhu-adam · Sep 6, 2024 · 66c2bfa · 66c2bfa
1 parent 3c33172
commit 66c2bfa
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 1 deletion.
diff --git a/Game/Metadata/Tactic.lean b/Game/Metadata/Tactic.lean
@@ -1,4 +1,5 @@
 import Game.Metadata.Tactic.ByCases
+import Game.Metadata.Tactic.Constructor
 import Game.Metadata.Tactic.Induction
-import Game.Metadata.Tactic.Ring
 import Game.Metadata.Tactic.LinearCombination
+import Game.Metadata.Tactic.Ring
diff --git a/Game/Metadata/Tactic/Constructor.lean b/Game/Metadata/Tactic/Constructor.lean
@@ -0,0 +1,11 @@
+import Mathlib.Tactic.Ring
+
+namespace Game
+
+@[inherit_doc Lean.Parser.Tactic.constructor]
+macro (name := constructor) "constructor" : tactic =>
+  `(tactic| fconstructor)
+
+extend_docs Game.constructor after "The variant used in the Robo game is called
+`fconstructor` in Mathlib. The only difference is the real `constructor` sorts
+the goals in a way not ideal for the game."