list
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
as
:
A
List.
as
= nil
||
as
||
1
[length_of_not_nil]
cites the following:
Thm*
h
:
T
,
t
:
T
List.
h
.
t
= nil
[cons_neq_nil]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
list
1
Sections
StandardLIB
Doc
as:A List. 
as = nil 
||as||
1h:T, t:T List. h.t = nilas:A List. as = nil ||as||1h:T, t:T List. h.t = nil