Zulip Chat Archive

Stream: general

Topic: underhanded lean


view this post on Zulip Mario Carneiro (Dec 27 2018 at 01:44):

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

view this post on Zulip Keeley Hoek (Dec 27 2018 at 11:18):

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


Last updated: May 10 2021 at 17:39 UTC