(2steps total)
PrintForm
Definitions
list
1
Sections
StandardLIB
Search
Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
length
cons
A
:Type,
a
:
A
,
as
:
A
List. ||
a
.
as
|| = ||
as
||+1
By:
UnivCD
Generated subgoal:
1
1.
A
: Type
2.
a
:
A
3.
as
:
A
List
||
a
.
as
|| = ||
as
||+1
1
step
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
list
1
Sections
StandardLIB
Search
Doc
A:Type, a:A, as:A List. ||a.as|| = ||as||+1
