Zulip Chat Archive

Stream: general

Topic: strange parsing

Mario Carneiro (May 19 2018 at 04:11):

I just discovered that this parses:

#printnat
-- inductive nat : Type
-- constructors:
-- nat.zero : ℕ
-- nat.succ : ℕ → ℕ

I guess spaces are optional?

Kevin Buzzard (May 19 2018 at 13:43):

So what happens when one command happens to be a prefix of another one? What are all the commands? #print #exit #check #eval #reduce

Kevin Buzzard (May 19 2018 at 13:44):

#eval1+1 -- 2

Kevin Buzzard (May 19 2018 at 13:45):

#help

Kevin Buzzard (May 19 2018 at 13:45):

#helpoptions works

Kevin Buzzard (May 19 2018 at 13:45):

aah bingo #helpcommands

Kevin Buzzard (May 19 2018 at 13:52):

definition er_has_run_out_of_ink := 4

#printer_has_run_out_of_ink

Kevin Buzzard (May 19 2018 at 13:52):

well there you go

Kenny Lau (May 19 2018 at 13:52):

lol

Kevin Buzzard (May 19 2018 at 14:14):

I think it's possible to define new commands, because sometimes I can import something and then magically use #find. If I define #che then maybe this breaks #check. Can I just define # and break everything?

Sebastian Ullrich (May 19 2018 at 14:23):

No, the longest match wins

Last updated: Dec 20 2023 at 11:08 UTC