Nuprl Definition : is-list-fun
is-list-fun() == λis-list,t. eval u = t in if u is a pair then is-list (snd(u)) otherwise if u = Ax then tt otherwise ⊥
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,
lambda: λx.A[x]
Definitions occuring in definition :
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-fun
Latex:
is-list-fun() ==
\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{}
Date html generated:
2016_05_15-PM-10_09_39
Last ObjectModification:
2015_09_23-AM-08_22_25
Theory : eval!all
Home
Index