Nuprl Definition : ucont
ucont(F;M) == eval K = FAN(λn,s. if M n s then tt else inr (λx.Ax) fi ) in <K - 1, λ_,_,_. Ax>
Definitions occuring in Statement :
FAN: FAN(d),
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
btrue: tt,
apply: f a,
lambda: λx.A[x],
pair: <a, b>,
inr: inr x ,
subtract: n - m,
natural_number: $n,
axiom: Ax
Definitions occuring in definition :
callbyvalue: callbyvalue,
FAN: FAN(d),
ifthenelse: if b then t else f fi ,
apply: f a,
btrue: tt,
inr: inr x ,
pair: <a, b>,
subtract: n - m,
natural_number: $n,
lambda: λx.A[x],
axiom: Ax
FDL editor aliases :
ucont
Latex:
ucont(F;M) == eval K = FAN(\mlambda{}n,s. if M n s then tt else inr (\mlambda{}x.Ax) fi ) in <K - 1, \mlambda{}$_\mbackslash{}ff7\000Cb}$,$_{}$,$_{}$. Ax>
Date html generated:
2019_06_20-PM-02_52_33
Last ObjectModification:
2019_01_27-PM-02_03_04
Theory : continuity
Home
Index