Nuprl Definition : binary-tree_ind

binary-tree_ind(v;
                btr_Leaf(val)⇒ Leaf[val];
                btr_Node(left,right)⇒ rec1,rec2.Node[left; right; rec1; rec2])  ==
  fix((λbinary-tree_ind,v. let lbl,v1 = v 
                           in if lbl="Leaf" then Leaf[v1]
                              if lbl="Node"
                                then let left,v2 = v1 
                                     in Node[left; v2; binary-tree_ind left; binary-tree_ind v2]
                              else ⊥
                              fi )) 
  v


Definitions occuring in Statement :  bottom: ⊥,  atom_eq: if a=b then c else d fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  token: "$token"
FDL editor aliases :  binary-tree_ind
binary-tree\_ind(v;
                                btr\_Leaf(val){}\mRightarrow{}  Leaf[val];
                                btr\_Node(left,right){}\mRightarrow{}  rec1,rec2.Node[left;  right;  rec1;  rec2])    ==
    fix((\mlambda{}binary-tree$_{ind}$,v.  let  lbl,v1  =  v 
                                                    in  if  lbl="Leaf"  then  Leaf[v1]
                                                          if  lbl="Node"
                                                              then  let  left,v2  =  v1 
                                                                        in  Node[left;  v2;  binary-tree$_{ind}$  left;  \000Cbinary-tree$_{ind}$  v2]
                                                          else  \mbot{}
                                                          fi  )) 
    v


Date html generated: 2015_07_17-AM-07_52_21
Last ObjectModification: 2014_05_06-AM-10_19_46

Home Index