Nuprl Definition : binary_map_ind

binary_map_ind(v;E;key,value,cnt,left,right,rec1,rec2.T[key;value;cnt;left;right;rec1;rec2]) ==
  fix((λbinary_map_ind,v. let lbl,v1 = v 
                          in if lbl="E" then E
                             if lbl="T"
                               then let key,v2 = v1 
                                    in let value,v3 = v2 
                                       in let cnt,v4 = v3 
                                          in let left,v5 = v4 
                                             in T[key;value;cnt;left;v5;binary_map_ind left;binary_map_ind v5]
                             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
FDL editor aliases :  binary_map_ind
Latex:
binary\_map\_ind(v;E;key,value,cnt,left,right,rec1,rec2.T[key;value;cnt;left;right;rec1;rec2])  ==
    fix((\mlambda{}binary\_map$_{ind}$,v.  let  lbl,v1  =  v 
                                                  in  if  lbl="E"  then  E
                                                        if  lbl="T"
                                                            then  let  key,v2  =  v1 
                                                                      in  let  value,v3  =  v2 
                                                                            in  let  cnt,v4  =  v3 
                                                                                  in  let  left,v5  =  v4 
                                                                                        in  T[key;value;cnt;left;v5;binary\_map$_{ind\mbackslash{}\000Cff7d$ 
                                                                                                                                              left;binary\_map$_\mbackslash{}ff7\000Cbind}$  v5]
                                                        else  Ax
                                                        fi  )) 
    v


Date html generated: 2016_05_17-PM-01_37_44
Last ObjectModification: 2015_12_14-PM-01_55_58

Theory : binary-map


Home Index