Notation for RelDecl breaks core rocq syntax #152
Description
Notation "a ?[ r ] b" := (rel_dec a b).
breaks the syntax for creating existentials inline, i.e.
fun (x : ?[X]) => x cannot be parsed any more.
{{ message }}
Notation "a ?[ r ] b" := (rel_dec a b).
breaks the syntax for creating existentials inline, i.e.
fun (x : ?[X]) => x cannot be parsed any more.