(6steps total)
PrintForm
Definitions
Lemmas
list
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
map
select
A
,
B
:Type,
f
:(
A
B
),
as
:
A
List,
n
:
||
as
||. map(
f
;
as
)[
n
] =
f
(
as
[
n
])
By:
UnivCD
Generated subgoal:
1
1.
A
: Type
2.
B
: Type
3.
f
:
A
B
4.
as
:
A
List
5.
n
:
||
as
||
map(
f
;
as
)[
n
] =
f
(
as
[
n
])
5
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
Lemmas
list
1
Sections
StandardLIB
Doc
A,B:Type, f:(A
B), as:A List, n:
||as||. map(f;as)[n] = f(as[n]) A,B:Type, f:(AB), as:A List, n:||as||. map(f;as)[n] = f(as[n])B
||as||
map(f;as)[n] = f(as[n])
