Definitions
hol
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
eq_pred
Def
eq(
'a
) == {
f
:(
'a
'a
)|
f
= (
x
:
'a
.
y
:
'a
.
x
=
y
) }
Thm*
'a
:Type. eq(
'a
)
Type
subtype
Def
S
T
==
x
:
S
.
x
T
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
hol
Sections
HOLlib
Doc
'a
)| f = (
x:'a. y:'a. x =
y) }
'a:Type. eq('a) 
Type
T == x:S. x T'a)| f = (x:'a. y:'a. x = y) }'a:Type. eq('a) Type T == x:S. x T
