Nuprl Definition : ev-list
ev-list(t;f) ==
fix((λev-list,t,f. eval u = t in
if u is a pair then let a,b = u
in ev-list b (λc.(f <a, c>)) otherwise if u = Ax then f Ax otherwise ⊥))
t
f
Definitions occuring in Statement :
bottom: ⊥,
callbyvalue: callbyvalue,
ispair: if z is a pair then a otherwise b,
isaxiom: if z = Ax then a otherwise b,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
axiom: Ax
Definitions occuring in definition :
fix: fix(F),
callbyvalue: callbyvalue,
ispair: if z is a pair then a otherwise b,
spread: spread def,
lambda: λx.A[x],
pair: <a, b>,
isaxiom: if z = Ax then a otherwise b,
apply: f a,
axiom: Ax,
bottom: ⊥
FDL editor aliases :
ev-list
Latex:
ev-list(t;f) ==
fix((\mlambda{}ev-list,t,f. eval u = t in
if u is a pair then let a,b = u
in ev-list b (\mlambda{}c.(f <a, c>))
otherwise if u = Ax then f Ax otherwise \mbot{}))
t
f
Date html generated:
2016_05_15-PM-10_08_59
Last ObjectModification:
2015_09_23-AM-08_22_23
Theory : eval!all
Home
Index