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
Definitions occuring in definition :
list_accum: list_accum,
callbyvalueall: callbyvalueall,
mFOL-freevars: mFOL-freevars(fmla),
callbyvalue: callbyvalue,
bigger-int: bigger-int(n;L),
natural_number: $n
FDL editor aliases :
new-mFO-var
Latex:
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:
2016_05_15-PM-10_30_58
Last ObjectModification:
2015_09_23-AM-08_25_56
Theory : minimal-first-order-logic
Home
Index