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.
flatten
Def
flatten(
l
) == if null(
l
) then nil else head(
l
) @ flatten(tl(
l
)) fi
Def
(recursive)
Thm*
'a
:Type,
l
:(
'a
List) List. flatten(
l
)
'a
List
label
Def
t
...$L ==
t
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
hol
list
1
Sections
HOLlib
Doc
'a:Type, l:('a List) List. flatten(l) 
'a List'a:Type, l:('a List) List. flatten(l) 'a List
