underhanded lean

Stream: general

[Mario Carneiro]

wow, I didn't expect this to work:

open lean.parser interactive interactive.types

@[user_command] meta def my_print (_ : parse $ tk "#print") : lean.parser unit :=
tk "axioms" >> ident $> trace "totally ok" ().

@[user_command] meta def my_def (_ : parse $ tk "def") : lean.parser unit :=
ident >> tk ":" >> texpr >> tk ":=" >> ident $> trace "looks good to me" ().

def contradiction : false := sure -- looks good to me
#print axioms contradiction -- totally ok

Apparently you can override basically all lean command tokens, including section, namespace, def and end

[Keeley Hoek]

Yep
At one point I tried a sneaky 'begin' override, but the problem is you can never close a block you open