rename iGiveUpAx to xyzzyAxiom

leanprover-community · Mar 14, 2024 · d6bf568 · d6bf568
1 parent 1a66069
commit d6bf568
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Game/Tactic/Xyzzy.lean b/Game/Tactic/Xyzzy.lean
@@ -3,11 +3,11 @@ import Lean
 universe u
 
 @[never_extract]
-axiom iGiveUpAx (α : Sort u) (synthetic := false) : α
+axiom xyzzyAxiom (α : Sort u) (synthetic := false) : α
 
 /--
 `xyzzy` is an ancient magic word, believed to be the root of the
 modern word `sorry`. The game won't complain - or notice - if you
 prove anything with `xyzzy`.
 -/
-macro "xyzzy" : tactic => `(tactic| exact @iGiveUpAx _ false)
+macro "xyzzy" : tactic => `(tactic| exact @xyzzyAxiom _ false)