The Coq mailing list

[���� <hskiowa AT kaist.ac.kr>]

Dear coq-club:

 

I ran the following code in CoqIde:

 

>>Notation "'atmost1' a : A , p" := (am1 (fun a:A=>p))
>> (at level 200, x ident, right associativity,
>>    format "'[' 'atmost1' '/ ' a : A , '/ ' p ']'").

>>

>>Lemma tt : forall (A:Type)(P:A->Prop), atmost1 a:A, P a.

 

only to find:

 

>>Syntax error: ':' expected after [constr:operconstr level 200] (in [constr:binder_constr]).

 

What's wrong?

I only followed the way "exists" notation was set up.

 

 

Hyung Sun Kim