Nuprl Definition : Kleene-M
Kleene-M(F) == λn,f. ν(e.F bound-domain(f;n;e)?e:x.<x, x>)
Definitions occuring in Statement :
bound-domain: bound-domain(f;n;e),
apply: f a,
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
lambda: λx.A[x],
apply: f a,
bound-domain: bound-domain(f;n;e),
pair: <a, b>
FDL editor aliases :
Kleene-M
Latex:
Kleene-M(F) == \mlambda{}n,f. \mnu{}(e.F bound-domain(f;n;e)?e:x.<x, x>)
Date html generated:
2019_06_20-PM-02_50_44
Last ObjectModification:
2019_02_08-PM-03_08_10
Theory : continuity
Home
Index