coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] problem with notation

From: Sandrine Blazy <Sandrine.Blazy AT inria.fr>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] problem with notation
Date: Fri, 15 Oct 2004 14:42:19 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Dear all,

What is wrong with the following Axiom?

Check BL.E.eq.
BL.E.eq : BL.E.t -> BL.E.t -> Prop

Axiom B_eq_dec: forall x y: Bl,
  {BL.E.eq x y}+{~BL.E.eq x y}.
                       ^
                       Syntax error: 'with' expected after
[constr:operconstr level 200] (in [constr:operconstr])

Thanks in advance for any help,

Best regards,

Sandrine Blazy

[Coq-Club] problem with notation, Sandrine Blazy