coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Eduardo Gimenez <Eduardo.Gimenez AT trusted-logic.fr>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] Notation
- Date: Fri, 1 Oct 2004 16:48:25 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
- Organization: Trusted Logic
Hello!
What is wrong in the following definition?
Record R : Set := BR {
r_nat : nat;
r_bool: bool
}.
Notation "'function' n b '=>' e" :=
(fun r => match r with (BR n b) => e end) (at level 200).
Check (function n b => b).
> Syntax error: [constr:operconstr level 200] expected after
> [constr:operconstr level 200] (in [constr:binder_constr])
Thanks in advance for any help.
Best regards,
Eduardo.
- [Coq-Club] Notation, Eduardo Gimenez
- Re: [Coq-Club] Notation, Hugo Herbelin
Archive powered by MhonArc 2.6.16.