WhoCites
Definitions
hol
list
2
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites length?
length
Def ||
as
|| == Case of
as
; nil
0 ;
a
.
as'
||
as'
||+1 (recursive)
Thm*
A
:Type,
l
:
A
List. ||
l
||
Thm*
||nil||
Thm*
'a
:Type,
l
:
'a
List. ||
l
||
Syntax:
||
as
||
has structure:
length(
as
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
hol
list
2
Sections
HOLlib
Doc
0 ; a.as' ||as'||+1 (recursive)
A:Type, l:A List. ||l|| 
'a:Type, l:'a List. ||l|| 
0 ; a.as' ||as'||+1 (recursive)A:Type, l:A List. ||l|| 'a:Type, l:'a List. ||l|| 
