Nuprl Definition : pv11_p1_max

Nuprl Definition : pv11_p1_max_bnum

pv11_p1_max_bnum(ldrs_uid) == λbn1,bn2. if pv11_p1_leq_bnum(ldrs_uid) bn1 bn2 then bn2 else bn1 fi

Definitions occuring in Statement : pv11_p1_leq_bnum: pv11_p1_leq_bnum(ldrs_uid), ifthenelse: if b then t else f fi , apply: f a, lambda: λx.A[x]
FDL editor aliases : pv11_p1_max_bnum

Latex:
pv11\_p1\_max\_bnum(ldrs$_{uid}$) == \mlambda{}bn1,bn2. if pv11\_p1\_leq\_bnum(ldrs$_\mbackslash{}\000Cff7buid}$) bn1 bn2 then bn2 else bn1 fi Date html generated: 2015_07_23-PM-04_11_14 Last ObjectModification: 2014_11_26-AM-11_22_38 Home Index