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 Ax
                              fi )) 
  v


Definitions occuring in Statement :  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",  axiom: Ax
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  atom_eq: if a=b then c else d fi ,  token: "$token",  spread: spread def,  apply: f a,  axiom: Ax
FDL editor aliases :  binary-tree_ind
Latex:
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  Ax
                                                          fi  )) 
    v


Date html generated: 2016_05_16-AM-09_07_13
Last ObjectModification: 2015_12_14-PM-01_41_38

Theory : C-semantics


Home Index