The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Dear all,

If a notations wizard could help me at defining

the following recursive notation in Coq, I would

be very grateful.

x ⪯ y ⪯ .. ⪯ z := red x y /\ y ⪯ .. ⪯ z

where red : _ -> _ -> Prop

ie

a ⪯ b ⪯ c ⪯ d would be (red a b) /\ (red b c /\ red c d).

Sequences must have length >=2 (otherwise they would be meaningless)

Thank you very much for some insights,

Dominique