Definitions
hol
list
1
Sections
HOLlib
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
mt
Def
mt(
l
) == Case of
l
; nil
True ;
a
.
as'
False
Thm*
'a
:Type{i},
l
:
'a
List. mt(
l
)
Prop{1}
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
hol
list
1
Sections
HOLlib
Doc
P
A:Prop. Dec(A) 
Prop
True ; a.as' False'a:Type{i}, l:'a List. mt(l) Prop{1} PA:Prop. Dec(A) Prop True ; a.as' False'a:Type{i}, l:'a List. mt(l) Prop{1}
