Nuprl Definition : is-list-if-has-value-fun
is-list-if-has-value-fun(t;n) ==
primrec(n;λt.Unit;λm,T,t. if t is a pair then T (snd(t)) otherwise ↑isaxiom(t) supposing (t)↓) t
Definitions occuring in Statement :
primrec: primrec(n;b;c),
has-value: (a)↓,
assert: ↑b,
bfalse: ff,
btrue: tt,
uimplies: b supposing a,
pi2: snd(t),
ispair: if z is a pair then a otherwise b,
isaxiom: if z = Ax then a otherwise b,
unit: Unit,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
primrec: primrec(n;b;c),
unit: Unit,
lambda: λx.A[x],
uimplies: b supposing a,
has-value: (a)↓,
ispair: if z is a pair then a otherwise b,
apply: f a,
pi2: snd(t),
assert: ↑b,
isaxiom: if z = Ax then a otherwise b,
btrue: tt,
bfalse: ff
FDL editor aliases :
is-list-if-has-value-fun
Latex:
is-list-if-has-value-fun(t;n) ==
primrec(n;\mlambda{}t.Unit;\mlambda{}m,T,t. if t is a pair then T (snd(t)) otherwise \muparrow{}isaxiom(t) supposing (t)\mdownarrow{}) t
Date html generated:
2016_05_15-PM-10_08_26
Last ObjectModification:
2015_09_23-AM-08_22_22
Theory : eval!all
Home
Index