Nuprl Definition : prior
prior(n;f) ==
letrec rec(n)=if (n =z 0) then inr ⋅ else eval m = n - 1 in case f m of inl(x) => inl <m, x> | inr(z) => rec m fi in
rec
n
Definitions occuring in Statement :
natrec: natrec,
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
it: ⋅,
apply: f a,
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
inl: inl x,
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
natrec: natrec,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
inr: inr x ,
it: ⋅,
callbyvalue: callbyvalue,
subtract: n - m,
natural_number: $n,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inl: inl x,
pair: <a, b>,
apply: f a
FDL editor aliases :
prior
Latex:
prior(n;f) ==
letrec rec(n)=if (n =\msubz{} 0)
then inr \mcdot{}
else eval m = n - 1 in
case f m of inl(x) => inl <m, x> | inr(z) => rec m
fi in
rec
n
Date html generated:
2016_05_15-PM-03_25_48
Last ObjectModification:
2015_09_23-AM-07_43_12
Theory : general
Home
Index