I am using the ASCII turnstile |-
in a notation and now I realized that Ltac's match goal
no longer works. Is there a way to pick the right level for my coq-level |-
notation to avoid interfering with the parsing of ltac's match goal
?
I would try a combination of Locate "|-"
and Print Notation
of the results to try to understand what can be done in terms of parsing levels.
sadly the ltac notation does not show up in Locate
it's probably hard-coded somewhere, no idea how to figure out its level
not sure if it's even a level thing, ltac should be its own non-terminal in the grammar, no?
Maybe Print Grammar
, otherwise grep the mlg files in Coq sources?
I should probably first produce a minimal example, I realized there's more interactions here than I originally though
Is this about https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/bi/ascii.v ? At bedrock we're still using |-- instead, possibly out of caution for this problem.
so this came up in the coq files for my class
yeah here is a reproducer
Reserved Notation "Gamma |- e : A" (at level 74, e, A at next level).
Goal True.
repeat match goal with
[ H : _ = _ |- _ ] => clear H
end.
match goal with [ |- pattern ]
still works, but the moment I add a hypothesis it breaks
Pierre Roux said:
Maybe
Print Grammar
, otherwise grep the mlg files in Coq sources?
Print Grammar
says Error: Grammar not a defined object.
I have no idea what to look for in the mlg files...
It takes a while to get to the bottom of it but you can go via Print Grammar tactic
and work you way towards the actual parsing rules which eventually end up revealing that the term to the right of :
in H : ..
is parsed at level 200. It seems that putting your notation at a level > 200 fixes match goal
but I haven't tried actually using the notation for anything useful afterwards.
FWIW, if using a raw |-
is not feasible, you could just as well use a UTF8 symbol:
Reserved Notation "Gamma ⊢ e : A" (at level 74, e, A at next level).
or to keep ASCII style, you could tweak the token in an MathComp-like fashion, adding a prefix apostrophe… not so nice, but YMMV:
Reserved Notation "Gamma '|- e : A" (at level 74, e, A at next level).
this is in a teaching context, so Im avoiding unicode since I dont want to deal with all the trouble of students having to set up their editors for unicode input
yeah alternative notations are possible (|--
also comes to mind), but not this year, since I realized this after we already introduced the notation :joy:
@Janno yeah everything breaks when I put it at level 201...
is there any way to add parentheses in the match goal
that would resolve the ambiguity? I guess not, match goal
relies on |-
to not be in the follow set of constr
and that's just fundamentally incompatible with the notation we want.
Last updated: Oct 13 2024 at 01:02 UTC