Nuprl Definition : new-mFO-var
new-mFO-var(H) ==
accumulate (with value m and list item fmla):
let vs ←─ mFOL-freevars(fmla)
in eval n = bigger-int(m;vs) in
n
over list:
H
with starting value:
0)
Definitions occuring in Statement :
mFOL-freevars: mFOL-freevars(fmla),
bigger-int: bigger-int(n;L),
list_accum: list_accum,
callbyvalueall: callbyvalueall,
callbyvalue: callbyvalue,
natural_number: $n
FDL editor aliases :
new-mFO-var
new-mFO-var(H) ==
accumulate (with value m and list item fmla):
let vs \mleftarrow{}{} mFOL-freevars(fmla)
in eval n = bigger-int(m;vs) in
n
over list:
H
with starting value:
0)
Date html generated:
2015_07_17-AM-07_57_19
Last ObjectModification:
2013_04_19-AM-11_58_39
Home
Index