The Coq mailing list

[ldou AT cs.ecnu.edu.cn]

hi,guys,
    i'm using Coq to formalize the Sequence Diagram. The following inductive type of sequence diagram has been defined:

Inductive seqDiag:Set :=
|DE: event ->seqDiag
|DStrict:seqDiag->seqDiag->seqDiag
|DPar: seqDiag->seqDiag->seqDiag
|DSeq: seqDiag -> seqDiag ->seqDiag.

   Then i want to define "context" in Coq. According to our concept, a context is a sequence diagram with one of its fragment replaced by a special symbol x, just like term rewriting. how should i define "context"? any suggestions are appreciated.

----------------
===========================================================
Best regards!
 
ñ¼ÁÁ
»ª¶«Ê¦·¶´óѧ¼ÆËã»ú¿Æѧ¼¼Êõϵ
(Department of Computer Science, East China Normal University)

E-mail:ldou AT cs.ecnu.edu.cn   
 
===========================================================