Nuprl Definition : natrec
The 'natrec' operator ⌜letrec f(n)=g[n;f] in
f⌝ is really just the general recursion operator
⌜letrec f(n)=g[n;f] in
f ⌝,
but we "rename" it so that we can give a wf lemma specific to the
natural numbers.⋅
letrec f(n)=g[n; f] in f == letrec f(n)=g[n; f] in f
Definitions occuring in Statement :
genrec: genrec
Definitions occuring in definition :
genrec: genrec
FDL editor aliases :
natrec
Latex:
letrec f(n)=g[n; f] in f == letrec f(n)=g[n; f] in f
Date html generated:
2016_07_08-PM-04_47_25
Last ObjectModification:
2015_09_22-PM-05_45_46
Theory : int_1
Home
Index