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