---

ClassProgram ==
  A:Type
   X:EClass(A)
   {pg:eclass-program{i:l}(Message)| 
     (eclass-program-type(pg) = A)  (defined-class(pg) = X)} 

---

Definitions :  defined-class: defined-class(prg),  Message: Message,  eclass: EClass(A[eo; e]),  equal: s = t,  eclass-program-type: eclass-program-type(prg),  universe: Type,  and: P  Q,  eclass-program: eclass-program{i:l}(Info),  set: {x:A| B[x]} ,  product: x:A  B[x]
FDL editor aliases :  cdv-class-program

---

ClassProgram  ==
    A:Type
    \mtimes{}  X:EClass(A)
    \mtimes{}  \{pg:eclass-program\{i:l\}(Message)|  (eclass-program-type(pg)  =  A)  \mwedge{}  (defined-class(pg)  =  X)\} 


Date html generated: 2010_08_27-PM-08_14_22
Last ObjectModification: 2010_07_07-PM-03_35_55

Home Index