---

PropRule ==
  dv:ClassDerivation
   Name
   T:LimitedType
   P:T  
   Id  hd(cdv-types(dv))  {v:T| (P v)} 
   (hd(cdv-types(dv))  (Id List))

---

Definitions :  Id: Id,  list: type List,  cdv-types: cdv-types(dv),  hd: hd(l),  function: x:A  B[x],  apply: f a,  assert: b,  set: {x:A| B[x]} ,  product: x:A  B[x],  bool: ,  limited-type: LimitedType,  name: Name,  classderiv: ClassDerivation
FDL editor aliases :  prop-rule

---

PropRule  ==
    dv:ClassDerivation
    \mtimes{}  Name
    \mtimes{}  T:LimitedType
    \mtimes{}  P:T  {}\mrightarrow{}  \mBbbB{}
    \mtimes{}  Id  {}\mrightarrow{}  hd(cdv-types(dv))  {}\mrightarrow{}  \{v:T|  \muparrow{}(P  v)\} 
    \mtimes{}  (hd(cdv-types(dv))  {}\mrightarrow{}  (Id  List))


Date html generated: 2010_08_30-AM-12_56_42
Last ObjectModification: 2010_08_23-PM-01_14_32

Home Index