Definitions
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
int_seg
Def
{
i
..
j
} == {
k
:
|
i
k
<
j
}
Thm*
m
,
n
:
. {
m
..
n
}
Type
iter_via_intseg
Def
Iter(
f
;
u
)
i
:{
a
..
b
}.
e
(
i
)
Def
== if
a
<
b
f
((Iter(
f
;
u
)
i
:{
a
..
b
-1
}.
e
(
i
)),
e
(
b
-1)) else
u
fi
Def
(recursive)
Thm*
f
:(
A
A
A
),
u
:
A
,
a
,
b
:
,
e
:({
a
..
b
}
A
). (Iter(
f
;
u
)
i
:{
a
..
b
}.
e
(
i
))
A
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
IteratedBinops
Sections
DiscrMathExt
Doc