---

F(x) where 
F(0) = zero  
F(pre.body) = comm[pre; body; rec1] where  
               rec1 = F(body)   
F(left + right) = option[left; right; rec1; rec2] where  
                   rec1 = F(left)  
                   rec2 = F(right)  
F(left | right) = par[left; right; rec1; rec2] where  
                   rec1 = F(left)  
                   rec2 = F(right)  
F(!body) = rep[body; rec1] where  
            rec1 = F(body)  
F(new name.body) = new[name; body; rec1] where  
                    rec1 = F(body) ==
  Y 
  (pi_term_ind,x.
    case x
    of inl(x) => zero
     | inr(x) => case x
                 of inl(x) => comm[fst(x); snd(x); pi_term_ind (snd(x))]
                  | inr(x) => case x
                              of inl(x) => option[fst(x); snd(x); pi_term_ind 
                                                                  (fst(x)); ... 
                                                                            ...]
                               | inr(x) => case x
                                           of inl(x) => par[...; ...; ...; ... 
                                                                           ...]
                                            | inr(x) => case x
                                                        of inl(x) => rep[x; ... 
                                                                            x]
                                                         | inr(x) => ...) 
  x

---

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 :  pi_ind

---

F(x)  where 
F(0)  =  zero   
F(pre.body)  =  comm[pre;  body;  rec1]  where   
                              rec1  =  F(body)     
F(left  +  right)  =  option[left;  right;  rec1;  rec2]  where   
                                      rec1  =  F(left)   
                                      rec2  =  F(right)   
F(left  |  right)  =  par[left;  right;  rec1;  rec2]  where   
                                      rec1  =  F(left)   
                                      rec2  =  F(right)   
F(!body)  =  rep[body;  rec1]  where   
                        rec1  =  F(body)   
F(new  name.body)  =  new[name;  body;  rec1]  where   
                                        rec1  =  F(body)  ==
    Y 
    (\mlambda{}pi\_term$_{ind}$,x.
        case  x
        of  inl(x)  =>  zero
          |  inr(x)  =>  case  x
                                  of  inl(x)  =>  comm[fst(x);  snd(x);  pi\_term$_{ind}$  (snd(x))]
                                    |  inr(x)  =>  case  x
                                                            of  inl(x)  =>  option[fst(x);  snd(x);  pi\_term$_{ind}\mbackslash{}ff2\000C
4  (fst(x));  pi\_term$_{ind}$ 
                                                                                                                                                                              (snd(x))]
                                                              |  inr(x)  =>  case  x
                                                                                      of  inl(x)  =>  par[fst(x);  snd(x);  pi\_term$_{in\000C
d}$ 
                                                                                                                                                        (fst(x));  pi\_term$\mbackslash{}f\000C
f5f{ind}$ 
                                                                                                                                                                            (snd(x))]
                                                                                        |  inr(x)  =>  case  x
                                                                                                                of  inl(x)  =>  rep[x;  pi\_term$_{in\000C
d}$  x]
                                                                                                                  |  inr(x)  =>  new[fst(x);  snd(x);  pi\_term\mbackslash{}ff2\000C
4_{ind}$ 
                                                                                                                                                                                  (snd(x))]) 
    x


Date html generated: 2010_08_27-PM-08_37_16
Last ObjectModification: 2010_02_11-PM-06_48_52

Home Index