Zulip Chat Archive

Stream: general

Topic: tokens


view this post on Zulip Scott Morrison (Oct 08 2018 at 06:17):

Does anyone know where the list of "registered tokens" is?

/-- Check that the next token is tk and consume it. tk must be a registered token. -/
meta constant tk (tk : string) : parser unit

view this post on Zulip Simon Hudon (Oct 08 2018 at 06:18):

You can define one as precedence `my_keyword`:0

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Oct 08 2018 at 06:21):

However ? isn't an allowed token.

view this post on Zulip Scott Morrison (Oct 08 2018 at 06:21):

Do you have a suggestion for good syntax for this?

view this post on Zulip 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?.

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Oct 08 2018 at 06:25):

? was meant to be a parameter

view this post on Zulip Scott Morrison (Oct 08 2018 at 06:25):

I can make this work with !, just via:

view this post on Zulip Scott Morrison (Oct 08 2018 at 06:25):

meta def backwards_reasoning (trace : parse $ optional (tk "!")) ...

view this post on Zulip Scott Morrison (Oct 08 2018 at 06:26):

Hmm, it seems # works fine, maybe that's good enough.

view this post on Zulip Mario Carneiro (Oct 08 2018 at 06:26):

Surely ? is a token

view this post on Zulip 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"

view this post on Zulip Mario Carneiro (Oct 08 2018 at 06:26):

I think rcases and rintro use ? in their parsing, for the hint mode

view this post on Zulip Scott Morrison (Oct 08 2018 at 06:27):

Okay, I will look at those.

view this post on Zulip Mario Carneiro (Oct 08 2018 at 06:27):

Actually it would be nice if squeeze_simp was simp?

view this post on Zulip Scott Morrison (Oct 08 2018 at 06:28):

Ugh...

view this post on Zulip Simon Hudon (Oct 08 2018 at 06:28):

I get the same error as you but this fixes it:

precedence `?`:0

view this post on Zulip Scott Morrison (Oct 08 2018 at 06:28):

Awesome, thanks @Simon Hudon.

view this post on Zulip Scott Morrison (Oct 08 2018 at 06:28):

Presumably this is a bit fragile, but works for now. :-)

view this post on Zulip Mario Carneiro (Oct 08 2018 at 06:28):

I would be careful with that

view this post on Zulip Mario Carneiro (Oct 08 2018 at 06:29):

declaring something as a token makes it unusable as a variable name

view this post on Zulip Mario Carneiro (Oct 08 2018 at 06:29):

maybe that's not a problem here though :)

view this post on Zulip Mario Carneiro (Oct 08 2018 at 06:30):

Does it work if you declare it locally?

view this post on Zulip 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

view this post on Zulip Simon Hudon (Oct 08 2018 at 06:33):

I am also unclear on the interaction between postfix and precedence

view this post on Zulip Scott Morrison (Oct 08 2018 at 06:36):

You can't do anything with local precedence

view this post on Zulip Simon Hudon (Oct 08 2018 at 06:37):

Even if you could that would make your tactic tricky to use

view this post on Zulip Scott Morrison (Oct 08 2018 at 06:38):

Yeah.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 16:19):

oh! I didn't realize rcases? was broken

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 17:41):

was it? I don't recall any error reports for rcases?

view this post on Zulip Patrick Massot (Oct 08 2018 at 18:03):

e.g. https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/rcases.3F/near/133503552

view this post on Zulip Mario Carneiro (Oct 08 2018 at 18:05):

oh, I thought that was resolved from the comments

view this post on Zulip 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: May 08 2021 at 10:12 UTC