---

case(x)
Base(args)=> base[args]
pair(fst,snd) => rec1,rec2.pair[fst; snd; rec1; rec2]
(X)'=> rec1.delay[X; dummy; rec1]
fun(arg:argtype):typ=> rec1.comb[typ; argtype; arg; fun; rec1]
fun(arg:argtype, self'):typ=> rec1.reccomb[typ; argtype; arg; fun; rec1] ==
  Y 
  (classderiv_ind,x.
    case x
    of inl(x) => base[x]
     | inr(x) => case x
                 of inl(x) => pair[fst(x); snd(x); classderiv_ind 
                                                   (fst(x)); classderiv_ind 
                                                             (snd(x))]
                  | inr(x) => case x
                              of inl(x) => delay[fst(x); snd(x); classderiv_ind 
                                                                 (fst(x))]
                               | inr(x) => case x
                                           of inl(x) => ...
                                            | inr(x) => ...) 
  x

---

Definitions :  ycomb: Y,  lambda: x.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  apply: f a,  pi1: fst(t),  pi2: snd(t)
FDL editor aliases :  classderiv_ind classderiv_ind

---

case(x)
Base(args)=>  base[args]
pair(fst,snd)  =>  rec1,rec2.pair[fst;  snd;  rec1;  rec2]
(X)'=>  rec1.delay[X;  dummy;  rec1]
fun(arg:argtype):typ=>  rec1.comb[typ;  argtype;  arg;  fun;  rec1]
fun(arg:argtype,  self'):typ=>  rec1.reccomb[typ;  argtype;  arg;  fun;  rec1]  ==
    Y 
    ... 
    x


Date html generated: 2010_08_27-PM-08_08_10
Last ObjectModification: 2010_06_18-PM-04_22_23

Home Index