PrintForm
Definitions
list
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
length
of
null
list
A
:Type,
as
:
A
List.
as
= nil
||
as
|| = 0
By:
UnivCD THEN (HypSubst -1 0) THEN (AbReduce 0)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
list
1
Sections
StandardLIB
Doc
A:Type, as:A List. as = nil 
||as|| = 0 A:Type, as:A List. as = nil ||as|| = 0
