Nuprl Definition : l-exists-decider
l-exists-decider() ==
λL,dcd. eval j' = ||L|| in
letrec G(x)=if (x) < (j')
then case dcd L[x] of inl(z) => inl <x, z> | inr(z) => G (x + 1)
else (inr (λx.Ax) ) in
G(0)
Definitions occuring in Statement :
select: L[n],
length: ||as||,
genrec-ap: genrec-ap,
callbyvalue: callbyvalue,
less: if (a) < (b) then c else d,
apply: f a,
lambda: λx.A[x],
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
inl: inl x,
add: n + m,
natural_number: $n,
axiom: Ax
Definitions occuring in definition :
callbyvalue: callbyvalue,
length: ||as||,
genrec-ap: genrec-ap,
less: if (a) < (b) then c else d,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
select: L[n],
inl: inl x,
pair: <a, b>,
apply: f a,
add: n + m,
inr: inr x ,
lambda: λx.A[x],
axiom: Ax,
natural_number: $n
FDL editor aliases :
l-exists-decider
Latex:
l-exists-decider() ==
\mlambda{}L,dcd. eval j' = ||L|| in
letrec G(x)=if (x) < (j')
then case dcd L[x] of inl(z) => inl <x, z> | inr(z) => G (x + 1)
else (inr (\mlambda{}x.Ax) ) in
G(0)
Date html generated:
2016_05_14-AM-07_47_55
Last ObjectModification:
2015_09_22-PM-05_54_00
Theory : list_1
Home
Index