The Coq mailing list

[Djamila Baroudi <baroudi.d7 AT gmail.com>]

hello;

I defines a new type called "event" and I still have to define the relationship between these events like the sequence between two events, which means that event e2 can not happen unless the event e1 is checked.

Inductive event:Type:=send(msg:string)

| receive(msg:string)

I try this but it's incorrect:

Inductive activity:Type:=

evenement(_:event).

|sequence (e1 e2 : event) : bool := e1 && e2.

can you help me please? n

Thank you.

--

Mlle Djamila Baroudi                           

Faculté des Sciences Exactes et Informatique,        

Université de Mostaganem,

27000 Mostaganem, Algérie.