---

case(x)
  var(name)=>var[name]
  basic(val)=>basic[val]
  operator(name)=>op[name]
  fun(arg)=>rec1,rec2.apply[fun; arg; rec1; rec2]
  lambda v1. body=>rec1.lambda[v1; body; rec1]
  let lhs = rsh in body=> rec1,rec2.let[lhs; rsh; body; rec1; rec2]) ==
  Y 
  (esharp_exp_ind,x.
    case x
    of inl(x) =>
     var[x]
     | inr(x) =>
     case x
     of inl(x) =>
      basic[x]
      | inr(x) =>
      case x
      of inl(x) =>
       op[x]
       | inr(x) =>
       case x
       of inl(x) =>
        apply[fst(x); snd(x); esharp_exp_ind (fst(x)); esharp_exp_ind (snd(x))]
        | inr(x) =>
        case x
        of inl(x) =>
         lambda[fst(x); snd(x); esharp_exp_ind (snd(x))]
         | inr(x) =>
         let[fst(x); fst(snd(x)); snd(snd(x)); esharp_exp_ind 
                                               (fst(snd(x))); esharp_exp_ind 
                                                              (snd(snd(x)))]) 
  x

---

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

---

case(x)
    var(name)=>var[name]
    basic(val)=>basic[val]
    operator(name)=>op[name]
    fun(arg)=>rec1,rec2.apply[fun;  arg;  rec1;  rec2]
    lambda  v1.  body=>rec1.lambda[v1;  body;  rec1]
    let  lhs  =  rsh  in  body=>  rec1,rec2.let[lhs;  rsh;  body;  rec1;  rec2])  ==
    Y 
    (\mlambda{}esharp\_exp$_{ind}$,x.
        case  x
        of  inl(x)  =>
          var[x]
          |  inr(x)  =>
          case  x
          of  inl(x)  =>
            basic[x]
            |  inr(x)  =>
            case  x
            of  inl(x)  =>
              op[x]
              |  inr(x)  =>
              case  x
              of  inl(x)  =>
                apply[fst(x);  snd(x);  esharp\_exp$_{ind}$  (fst(x));  esharp\_exp$_\mbackslash{}\000Cff7bind}$  (snd(x))]
                |  inr(x)  =>
                case  x
                of  inl(x)  =>
                  lambda[fst(x);  snd(x);  esharp\_exp$_{ind}$  (snd(x))]
                  |  inr(x)  =>
                  let[fst(x);  fst(snd(x));  snd(snd(x));  esharp\_exp$_{ind}$  (fst(snd(x)));\000C  esharp\_exp$_{ind}$ 
                                                                                                                                                        (snd(snd(x)))]) 
    x


Date html generated: 2011_08_17-PM-05_14_11
Last ObjectModification: 2011_02_03-PM-04_32_34

Home Index