Nuprl Definition : l_tree_ind

l_tree_ind(v;
           l_tree_leaf(val)⇒ leaf[val];
           l_tree_node(val,left_subtree,right_subtree)⇒ rec1,rec2.node[val; left_subtree; right_subtree; rec1;
                                                                        rec2])  ==
  fix((λl_tree_ind,v. let lbl,v1 = v 
                      in if lbl="leaf" then leaf[v1]
                         if lbl="node"
                           then let val,v2 = v1 
                                in let left_subtree,v3 = v2 
                                   in node[val; left_subtree; v3; l_tree_ind left_subtree; l_tree_ind v3]
                         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 :  l_tree_ind
l\_tree\_ind(v;
                      l\_tree\_leaf(val){}\mRightarrow{}  leaf[val];
                      l\_tree\_node(val,left$_{subtree}$,right$_{subtree}\mbackslash{}ff2\000C4){}\mRightarrow{}  rec1,rec2.node[val;  left$_{subtree}$;
                                                                                                                                            right$_{subtree\mbackslash{}ff\000C7d$;  rec1;  rec2])    ==
    fix((\mlambda{}l\_tree$_{ind}$,v.  let  lbl,v1  =  v 
                                          in  if  lbl="leaf"  then  leaf[v1]
                                                if  lbl="node"
                                                    then  let  val,v2  =  v1 
                                                              in  let  left$_{subtree}$,v3  =  v2 
                                                                    in  node[val;  left$_{subtree}$;  v3;  l\_tree$\000C_{ind}$  left$_{subtree}$;  l\_tree$_{ind}$  v3]
                                                else  \mbot{}
                                                fi  )) 
    v


Date html generated: 2015_07_17-AM-07_41_41
Last ObjectModification: 2014_05_05-PM-02_29_31

Home Index