(3steps total)
PrintForm
Definitions
list
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
map
id
A
:Type,
as
:
A
List. map(Id;
as
) =
as
By:
RepD THEN (OnVar `
as
' ListIndA) THEN (Reduce 0)
Generated subgoals:
1
1.
A
: Type
nil = nil
A
List
Auto
2
1.
A
: Type
2.
a
:
A
3.
as
:
A
List
4. map(Id;
as
) =
as
a
.map(Id;
as
) =
a
.
as
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
list
1
Sections
StandardLIB
Doc
A:Type, as:A List. map(Id;as) = as A:Type, as:A List. map(Id;as) = as nil = nil 
A List
a.map(Id;as) = a.as
