rename iGiveUpAx to xyzzyAxiom

This commit is contained in:
Jon Eugster
2024-03-14 10:38:41 +01:00
parent 1a66069e89
commit d6bf5686bc

View File

@@ -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)