ident_ parser

Stream: general

[Johan Commelin]

We have

/-- Parse an identifier or a '_' -/
meta def ident_ : parser name := ident <|> tk "_" *> return `_

Would it be possible to make this parser also accept French-quoted hypotheses such as ‹x ≠ y›?

[Eric Wieser]

That wouldn't be a parser name any more

[Eric Wieser]

What would intro ‹x ≠ y› mean?

[Johan Commelin]

Hmm, that makes sense.

[Johan Commelin]

So I guess I want a new kind of parser, that takes a name or a french quoted thingy.

[Eric Wieser]

If this is regarding library_search, then it sounds like the problem is you're parsing a name but should be parsing an expression

[Eric Wieser]

Presumbly h x should be valid in your intended use case too?

[Johan Commelin]

hmmz, probably. This is quickly becoming too meta. But I guess library_search using [h x] is reasonable.

[Eric Wieser]

how does tactic#simpa parse the using clause?

[Eric Wieser]

I think that's what you want here

[Rob Lewis]

library_search using [t1, t2] should probably just add t1, t2 to the context if they aren't local constants already, then you don't have to change the main function at all

[Eric Wieser]

Would we need the kinda of metavariable avoidance used by simpa here?

https://github.com/leanprover-community/mathlib/blob/f87478329d165cbd45631d806d5ae3ff061909a7/src/tactic/simpa.lean#L36-L54

[Johan Commelin]

But library_search needs to filter it's results to see if they make use of t1 and t2. Is that easy if they are arbitrary expressions?

[Rob Lewis]

Parse an optional tk "using" >> pexpr_list, elaborate the list, note_anon anything in the list that isn't a local constant. Then you just have a list of local constants

[Johan Commelin]

If you say so... :rofl:

[Rob Lewis]

Actually, this will cause trouble when it prints out what it finds at the end