---

ClassProgram(T) ==
  i:Id fp-> A:Type
             ks:{k:Knd| hasloc(k;i)}  List
             typ:{k:Knd| (k  ks)}   Type
             k:{k:Knd| (k  ks)}   typ k  A  (T + Top)
             A  k:{k:Knd| (k  ks)}   typ k  A
             A

---

Definitions :  fpf: a:A fp-> B[a],  Id: Id,  list: type List,  assert: b,  hasloc: hasloc(k;i),  universe: Type,  union: left + right,  top: Top,  product: x:A  B[x],  set: {x:A| B[x]} ,  l_member: (x  l),  Knd: Knd,  function: x:A  B[x],  apply: f a
FDL editor aliases :  class-program

---

ClassProgram(T)  ==
    i:Id  fp->  A:Type
                        \mtimes{}  ks:\{k:Knd|  \muparrow{}hasloc(k;i)\}    List
                        \mtimes{}  typ:\{k:Knd|  (k  \mmember{}  ks)\}    {}\mrightarrow{}  Type
                        \mtimes{}  k:\{k:Knd|  (k  \mmember{}  ks)\}    {}\mrightarrow{}  typ  k  {}\mrightarrow{}  A  {}\mrightarrow{}  (T  +  Top)
                        \mtimes{}  A  {}\mrightarrow{}  k:\{k:Knd|  (k  \mmember{}  ks)\}    {}\mrightarrow{}  typ  k  {}\mrightarrow{}  A
                        \mtimes{}  A


Date html generated: 2010_08_27-AM-09_35_37
Last ObjectModification: 2009_12_16-AM-01_26_41

Home Index