IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
array seg wf12 1. T : Type
2. i : 3. j : {i...}
4. a : [T]Array
5. a.l = i & a.u = j 6. m : {i..j}
7. n : {m..j}
a[m..n].l = m & a[m..n].u = n
By:
Unfolds [`array_seg`;`array_lb`;`array_ub`] 0
THEN
Rewrite (DepthC (pi1_evalC ORELSEC pi2_evalC)) 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
}
a[m..n].l = m & a[m..n].u = n
