(6steps total)
PrintForm
Definitions
list
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
length
tl
1
1.
A
: Type
2.
l
:
A
List
||
l
||
1
||tl(
l
)|| = ||
l
||-1
By:
Analyze 2
Generated subgoals:
1
||nil||
1
||tl(nil)|| = ||nil||-1
2
steps
2
3.
u
:
A
4.
v
:
A
List
||
u
.
v
||
1
||tl((
u
.
v
))|| = ||
u
.
v
||-1
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
list
1
Sections
StandardLIB
Doc
||l||
1 
||tl(l)|| = ||l||-1 ||l||1 ||tl(l)|| = ||l||-1 ||nil||1 ||tl(nil)|| = ||nil||-1
||u.v||1 ||tl((u.v))|| = ||u.v||-1
