WhoCites
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites sfa
doc
props
as
types
example1?
sfa_doc_props_as_types_example1
Def
f
zero beyond
x
==
y
:
.
x
<
y
f
(
y
) = 0
Thm*
x
:
,
f
:(
).
f
zero beyond
x
Prop
nat
Def
== {
i
:
| 0
i
}
Thm*
Type
le
Def
A
B
==
B
<
A
Thm*
i
,
j
:
. (
i
j
)
Prop
not
Def
A
==
A
False
Thm*
A
:Prop. (
A
)
Prop
Syntax:
f
zero beyond
x
has structure:
sfa_doc_props_as_types_example1(
x
;
f
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc