The Coq mailing list

[t x <txrev319 AT gmail.com>]

It sounds like you want "pair of A and B", which has type "A * B" and shorthand notation "(a, b)" where a:A and b:B.

On Mon, Jul 1, 2013 at 4:48 PM, Djamila baroudi <baroudi.d7 AT gmail.com> wrote:

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.