(5steps total)
PrintForm
Definitions
array
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
p
array
wf
1
1.
T
: Type
2.
i
:
3.
j
: {
i
...}
[
T
]Array{
i
..
j
}
Type{[i']}
By:
Unfold `p_array` 0
Generated subgoal:
1
{
a
:[
T
]Array |
a
.l =
i
&
a
.u =
j
}
Type{[i']}
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
array
1
Sections
StandardLIB
Doc
[T]Array{i..j
} 
Type{[i']}
[T]Array{i..j} Type{[i']} {a:[T]Array | a.l = i & a.u = j } Type{[i']}
