Nuprl Definition : fresh-cname
fresh-cname(I) == (fst(list-max(x.x;[1 / I]))) + 1
Definitions occuring in Statement :
list-max: list-max(x.f[x];L),
cons: [a / b],
pi1: fst(t),
add: n + m,
natural_number: $n
Definitions occuring in definition :
add: n + m,
pi1: fst(t),
list-max: list-max(x.f[x];L),
cons: [a / b],
natural_number: $n
FDL editor aliases :
fresh-cname
Latex:
fresh-cname(I) == (fst(list-max(x.x;[1 / I]))) + 1
Date html generated:
2016_05_20-AM-09_28_24
Last ObjectModification:
2015_09_23-AM-09_29_25
Theory : cubical!sets
Home
Index