---

case(x)
var(name)=>var[name]
const(ty)=>const[ty]
domainrange =>rec1,rec2.arrow[domain; range; rec1; rec2]
fst  snd =>rec1,rec2.prod[fst; snd; rec1; rec2]
left + right =>rec1,rec2.union[left; right; rec1; rec2]
kind list =>rec1.list[kind; rec1]
Class(kind) =>rec1.class[kind; rec1] ==
  Y 
  (simple_type_ind,x.
    case x
    of inl(x) =>
     var[x]
     | inr(x) =>
     case x
     of inl(x) =>
      const[x]
      | inr(x) =>
      case x
      of inl(x) =>
       arrow[fst(x); snd(x); simple_type_ind (fst(x)); simple_type_ind (snd(x))]
       | inr(x) =>
       case x
       of inl(x) =>
        prod[fst(x); snd(x); simple_type_ind (fst(x)); simple_type_ind (snd(x))]
        | inr(x) =>
        case x
        of inl(x) =>
         union[fst(x); snd(x); simple_type_ind (fst(x)); simple_type_ind 
                                                         (snd(x))]
         | inr(x) =>
         case x
         of inl(x) =>
          list[x; simple_type_ind x]
          | inr(x) =>
          class[x; simple_type_ind 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],  pi1: fst(t),  pi2: snd(t),  decide: case b of inl(x) => s[x] | inr(y) => t[y],  apply: f a
FDL editor aliases :  simple_type_ind simple_type_ind

---

case(x)
var(name)=>var[name]
const(ty)=>const[ty]
domain{}\mrightarrow{}range  =>rec1,rec2.arrow[domain;  range;  rec1;  rec2]
fst  \mtimes{}  snd  =>rec1,rec2.prod[fst;  snd;  rec1;  rec2]
left  +  right  =>rec1,rec2.union[left;  right;  rec1;  rec2]
kind  list  =>rec1.list[kind;  rec1]
Class(kind)  =>rec1.class[kind;  rec1]  ==
    Y 
    (\mlambda{}simple\_type$_{ind}$,x.
        case  x
        of  inl(x)  =>
          var[x]
          |  inr(x)  =>
          case  x
          of  inl(x)  =>
            const[x]
            |  inr(x)  =>
            case  x
            of  inl(x)  =>
              arrow[fst(x);  snd(x);  simple\_type$_{ind}$  (fst(x));  simple\_type$_\000C{ind}$  (snd(x))]
              |  inr(x)  =>
              case  x
              of  inl(x)  =>
                prod[fst(x);  snd(x);  simple\_type$_{ind}$  (fst(x));  simple\_type$_\000C{ind}$  (snd(x))]
                |  inr(x)  =>
                case  x
                of  inl(x)  =>
                  union[fst(x);  snd(x);  simple\_type$_{ind}$  (fst(x));  simple\_type$\mbackslash{}ff\000C5f{ind}$  (snd(x))]
                  |  inr(x)  =>
                  case  x  of  inl(x)  =>  list[x;  simple\_type$_{ind}$  x]  |  inr(x)  =>  class[x;\000C  simple\_type$_{ind}$  x]) 
    x


Date html generated: 2011_08_17-PM-04_42_05
Last ObjectModification: 2011_02_06-PM-04_02_54

Home Index