Nuprl Definition : pv8_p1_max_bnum

pv8_p1_max_bnum(ldrs_uid) ==  bn1,bn2.if pv8_p1_leq_bnum(ldrs_uid) bn1 bn2 then bn2 else bn1 fi 


Definitions occuring in Statement :  pv8_p1_leq_bnum: pv8_p1_leq_bnum(ldrs_uid),  ifthenelse: if b then t else f fi ,  apply: f a,  lambda: x.A[x]
FDL editor aliases :  pv8_p1_max_bnum pv8_p1_max_bnum
pv8\_p1\_max\_bnum(ldrs$_{uid}$)  ==    \mlambda{}bn1,bn2.if  pv8\_p1\_leq\_bnum(ldrs$_\mbackslash{}ff7\000Cbuid}$)  bn1  bn2  then  bn2  else  bn1  fi 


Date html generated: 2012_02_20-PM-07_14_27
Last ObjectModification: 2012_02_06-PM-01_36_58

Home Index