Nuprl Definition : pv11_p1_upd_bnum
pv11_p1_upd_bnum() == λbnum,loc. case bnum of inl(z) => let r,l = z in pv11_p1_mk_bnum() (r + 1) loc | inr(z) => bnum
Definitions occuring in Statement :
pv11_p1_mk_bnum: pv11_p1_mk_bnum(),
apply: f a,
lambda: λx.A[x],
spread: spread def,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
add: n + m,
natural_number: $n
FDL editor aliases :
pv11_p1_upd_bnum
Latex:
pv11\_p1\_upd\_bnum() ==
\mlambda{}bnum,loc. case bnum of inl(z) => let r,l = z in pv11\_p1\_mk\_bnum() (r + 1) loc | inr(z) => bnum
Date html generated:
2015_07_23-PM-04_10_48
Last ObjectModification:
2014_11_26-AM-11_21_51
Home
Index