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 tk and consume it. tk must 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?

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

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?

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: May 08 2021 at 10:12 UTC