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