Definitions
mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
decidable
Def
Dec(
P
) ==
P
P
Thm*
A
:Prop. Dec(
A
)
Prop
l_member
Def
(
x
l
) ==
i
:
.
i
<||
l
|| &
x
=
l
[
i
]
T
Thm*
T
:Type,
x
:
T
,
l
:
T
List. (
x
l
)
Prop
not
Def
A
==
A
False
Thm*
A
:Prop. (
A
)
Prop
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
mb
list
1
Sections
MarkB
generic
Doc