The Coq mailing list

[like <12like34xiongmao AT 163.com>]

Pierre Casteran <pierre.casteran <at> labri.fr> writes:

> 
> Hi,
> 
>    It's difficult to answer your question: I think it lacks some
> declarations of the operators that occur in t2 and tt2.
> 
> Pierre


All my notations are defined like this or in the fomula(mention before).
Definition and(p q: formula) : formula :=!(!p '|| !q).
Notation "p '&& q" :=(and p q) (at level 74, left associativity).

Definition chop(p:formula)(q:formula):= (cons p (cons q nil)) 'prj (empty).
Notation "p ; q" := (chop p q) (at level 75, right associativity).

I also try a simliar example in Prop and it works. I don't know what I lacks. 
Any
suggestions?