Nuprl Definition : int_seg_decide
int_seg_decide(d;i;j) ==
fix((λG,x. if (x) < (j) then case d x of inl(z) => inl <x, z> | inr(z) => G (x + 1) else (inr (λx.⋅) ))) i
Definitions occuring in Statement :
it: ⋅,
less: if (a) < (b) then c else d,
apply: f a,
fix: fix(F),
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
Definitions occuring in definition :
fix: fix(F),
less: if (a) < (b) then c else d,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inl: inl x,
pair: <a, b>,
apply: f a,
add: n + m,
natural_number: $n,
inr: inr x ,
lambda: λx.A[x],
it: ⋅
FDL editor aliases :
int_seg_decide
Latex:
int\_seg\_decide(d;i;j) ==
fix((\mlambda{}G,x. if (x) < (j)
then case d x of inl(z) => inl <x, z> | inr(z) => G (x + 1)
else (inr (\mlambda{}x.\mcdot{}) )))
i
Date html generated:
2016_05_13-PM-03_47_40
Last ObjectModification:
2015_09_22-PM-05_45_15
Theory : call!by!value_2
Home
Index