The Coq mailing list

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

Hello,

I'm PHD student, and i'm starter with coq, can you help me please, i have many problems with definitions of new types, and combination of these types.

i have for example this new type named predicate

Inductive predicate : Type:=

Etat(etat:Prop)

|variable(var:nat).

an other event 

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

| receive(msg:string)

| predicat_test(predicat:predicate). 

and i want defined an other one "activity_type" where this type is the conjunction of two events  (event1 /\ event2).

how to do this?

thank you

--

Mlle Djamila Baroudi                           

Faculté des Sciences Exactes et Informatique,        

Université de Mostaganem,

27000 Mostaganem, Algérie.