You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Elpi Program tutorial lp:{{
kind person type.
type mallory, bob, alice person.
}}.
This quotation mechanism lp:{{ ... }} is introduced by rocq-prover/rocq#9733. Since the delimiters can be nested, I think that we need a recursive grammar (CFG, PEG, etc.) to detect the end of commands, and couldn't write regexps like coq-end-command-regexp(-backward) anymore to detect it. But I wonder that PG handled the following command properly.
idtac (*(**) . *).
Does anyone have a workaround or fix for this problem?