Nuprl Definition : regextfun
regextfun(f;w)==r let t,g = w in λu.regextfun(f;g u)"(set-dom(f t))
regextfun(f;w) == fix((λregextfun,w. let t,g = w in λu.(regextfun (g u))"(set-dom(f t)))) w
Definitions occuring in Statement :
mk-set: f"(T),
set-dom: set-dom(s),
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def
Definitions occuring in definition :
apply: f a,
lambda: λx.A[x],
set-dom: set-dom(s),
mk-set: f"(T),
spread: spread def,
fix: fix(F)
FDL editor aliases :
regextfun
regextfun
Latex:
regextfun(f;w)==r let t,g = w in \mlambda{}u.regextfun(f;g u)"(set-dom(f t))
Latex:
regextfun(f;w) == fix((\mlambda{}regextfun,w. let t,g = w in \mlambda{}u.(regextfun (g u))"(set-dom(f t)))) w
Date html generated:
2018_07_29-AM-10_07_01
Last ObjectModification:
2018_07_20-PM-04_45_44
Theory : constructive!set!theory
Home
Index