Nuprl Definition : is-list
is-list(t) ==
fix((λis-list,t. eval u = t in if u is a pair then is-list (snd(u)) otherwise if u = Ax then tt otherwise ⊥)) t
Definitions occuring in Statement :
bottom: ⊥,
callbyvalue: callbyvalue,
btrue: tt,
pi2: snd(t),
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]
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
callbyvalue: callbyvalue,
ispair: if z is a pair then a otherwise b,
apply: f a,
pi2: snd(t),
isaxiom: if z = Ax then a otherwise b,
btrue: tt,
bottom: ⊥
FDL editor aliases :
is-list
Latex:
is-list(t) ==
fix((\mlambda{}is-list,t. eval u = t in
if u is a pair then is-list (snd(u)) otherwise if u = Ax then tt otherwise \mbot{}))
t
Date html generated:
2016_05_15-PM-10_07_27
Last ObjectModification:
2015_09_23-AM-08_22_20
Theory : eval!all
Home
Index