Nuprl Definition : add-nat-missing
add-nat-missing(i;s) ==
let max,missing = s
in if max <z i then <i, missing @ [max + 1, i)>
if (max =z i) then <max, missing>
else <max, remove-combine(λx.(x - i);missing)>
fi
Definitions occuring in Statement :
remove-combine: remove-combine(cmp;l),
from-upto: [n, m),
append: as @ bs,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
eq_int: (i =z j),
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
subtract: n - m,
add: n + m,
natural_number: $n
FDL editor aliases :
add-nat-missing
add-nat-missing(i;s) ==
let max,missing = s
in if max <z i then <i, missing @ [max + 1, i)>
if (max =\msubz{} i) then <max, missing>
else <max, remove-combine(\mlambda{}x.(x - i);missing)>
fi
Date html generated:
2015_07_17-AM-08_21_30
Last ObjectModification:
2013_04_01-PM-00_42_56
Home
Index