Zulip Chat Archive
Stream: general
Topic: tokens
Scott Morrison (Oct 08 2018 at 06:17):
Does anyone know where the list of "registered tokens" is?
/-- Check that the next token is
tkand consume it.tkmust be a registered token. -/
meta constant tk (tk : string) : parser unit
Simon Hudon (Oct 08 2018 at 06:18):
You can define one as precedence `my_keyword`:0
Scott Morrison (Oct 08 2018 at 06:20):
I'd like to modify some of my tactics so they print out a trace message of what they're doing.
Scott Morrison (Oct 08 2018 at 06:21):
My idea was to have, e.g. backwards_reasoning, but then be able to write backwards_reasoning? and get trace ouput.
Scott Morrison (Oct 08 2018 at 06:21):
However ? isn't an allowed token.
Scott Morrison (Oct 08 2018 at 06:21):
Do you have a suggestion for good syntax for this?
Scott Morrison (Oct 08 2018 at 06:22):
I'm hoping that one day this model might be widespread --- e.g. in Lean 4 we could even imagine your squeeze_simp just be callable by simp?.
Simon Hudon (Oct 08 2018 at 06:24):
Are you trying to make backwards_reasoning?the name of the tactic or is ? a parameter to backwards_reasoning?
Scott Morrison (Oct 08 2018 at 06:25):
? was meant to be a parameter
Scott Morrison (Oct 08 2018 at 06:25):
I can make this work with !, just via:
Scott Morrison (Oct 08 2018 at 06:25):
meta def backwards_reasoning (trace : parse $ optional (tk "!")) ...
Scott Morrison (Oct 08 2018 at 06:26):
Hmm, it seems # works fine, maybe that's good enough.
Mario Carneiro (Oct 08 2018 at 06:26):
Surely ? is a token
Scott Morrison (Oct 08 2018 at 06:26):
Somehow ! strikes me as a "work harder!" modifier to a tactic, rather than a "tell me more"
Mario Carneiro (Oct 08 2018 at 06:26):
I think rcases and rintro use ? in their parsing, for the hint mode
Scott Morrison (Oct 08 2018 at 06:27):
Okay, I will look at those.
Mario Carneiro (Oct 08 2018 at 06:27):
Actually it would be nice if squeeze_simp was simp?
Scott Morrison (Oct 08 2018 at 06:28):
Ugh...
Simon Hudon (Oct 08 2018 at 06:28):
I get the same error as you but this fixes it:
precedence `?`:0
Scott Morrison (Oct 08 2018 at 06:28):
Awesome, thanks @Simon Hudon.
Scott Morrison (Oct 08 2018 at 06:28):
Presumably this is a bit fragile, but works for now. :-)
Mario Carneiro (Oct 08 2018 at 06:28):
I would be careful with that
Mario Carneiro (Oct 08 2018 at 06:29):
declaring something as a token makes it unusable as a variable name
Mario Carneiro (Oct 08 2018 at 06:29):
maybe that's not a problem here though :)
Mario Carneiro (Oct 08 2018 at 06:30):
Does it work if you declare it locally?
Mario Carneiro (Oct 08 2018 at 06:30):
I see that rcases has local postfix `?`:9001 := optional, which may be a factor in why this works
Simon Hudon (Oct 08 2018 at 06:33):
I am also unclear on the interaction between postfix and precedence
Scott Morrison (Oct 08 2018 at 06:36):
You can't do anything with local precedence
Simon Hudon (Oct 08 2018 at 06:37):
Even if you could that would make your tactic tricky to use
Scott Morrison (Oct 08 2018 at 06:38):
Yeah.
Reid Barton (Oct 08 2018 at 15:17):
Aha interesting. So this explains why I could never get rcases? to work. It only works once I make ? some kind of notation.
Simon Hudon (Oct 08 2018 at 15:42):
That sounds like a probable explanation. @Mario Carneiro you may need to add precedence `?`:0 in mathlib
Mario Carneiro (Oct 08 2018 at 16:19):
oh! I didn't realize rcases? was broken
Patrick Massot (Oct 08 2018 at 17:39):
This was mentioned several times here, but I guess we need to learn to use GitHub issues instead of only relying on whining here
Mario Carneiro (Oct 08 2018 at 17:41):
was it? I don't recall any error reports for rcases?
Patrick Massot (Oct 08 2018 at 18:03):
e.g. https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/rcases.3F/near/133503552
Mario Carneiro (Oct 08 2018 at 18:05):
oh, I thought that was resolved from the comments
Patrick Massot (Oct 08 2018 at 18:08):
I was sure it was mentioned a couple more times but I can't find it
Last updated: Dec 20 2023 at 11:08 UTC