The Coq mailing list

[Antoine Voizard <voizard AT seas.upenn.edu>]

Hi again,

By exploring the output of Print Grammar constr, I managed to make it work with explicit levels:

Notation "{ x , y | P }" := (sig2el (fun x y => P)) (at level 0, x at level 99, y at level 99) : type_scope.

However, if anybody has some good guidelines for seamlessly integrating new notations with old ones, that'd be very helpful.

Antoine

On 2016-06-30 19:22, Antoine Voizard wrote:

Hi all,

I just ran into a problem that I already had a couple of times, and I can't figure out what I'm doing wrong. The general idea is that, when declaring a new notation close to some existing ones, all the sudden Coq's parser won't recognize the old ones, by looking exclusively for the new one.

In this case, I needed an "inlined" version of subsets of pair types (simpler to use than an actual {x : A * B | ...}), so I just adapted the stdlib code:

Inductive sig2el (A:Type) (B:Type) (P : A -> B -> Prop) : Type :=
    exist2el : forall (x : A) (y : B), P x y -> sig2el P.

Notation "{ x , y | P }" := (sig2el(fun x y => P)) : type_scope.

But then, the following gives a syntax error because Coq expects a comma (I tried changing the notation with other characters as well - same result)

Lemma in_dec : forall x L, {x `in` L} + {¬ x `in` L}.

Could you tell me what's the issue?

Thanks,
Antoine