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.
l_member
Def
(
x
l
) ==
i
:
.
i
<||
l
|| &
x
=
l
[
i
]
T
Thm*
T
:Type,
x
:
T
,
l
:
T
List. (
x
l
)
Prop
tidentity
Def
Id == Id
Thm*
A
:Type. Id
A
A
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
mb
list
1
Sections
MarkB
generic
Doc
l) == 
i:
. i<||l|| & x = l[i] T
T:Type, x:T, l:T List. (x l) PropA:Type. Id A
A l) == i:. i<||l|| & x = l[i] TT:Type, x:T, l:T List. (x l) PropA:Type. Id AA
