Def {i..j} == {k:| i  k < j }

is mentioned by

Thm* ll:(T List) List, n:||concat(ll)||. Thm* m:||ll||.  Thm* ||concat(firstn(m;ll))||n Thm* & n-||concat(firstn(m;ll))||<||ll[m]|| Thm* & concat(ll)[n] = ll[m][(n-||concat(firstn(m;ll))||)]	[select_concat]
Thm* L1,L2:Top List, n:(||L1||+1). firstn(n;L1 @ L2) ~ firstn(n;L1)	[firstn_append]
Thm* P:(TProp), A,B:T List. Thm* A = B  (i:||A||. P(A[i]))  A = B  {x:T| P(x) } List	[list-eq-set-type]
Thm* n:, x,y:n. x before y  upto(n)  x<y	[before-upto]
Thm* n,i:. i<n  (i  upto(n))	[member_upto2]
Thm* m:, n:m. upto(m)[n] = n	[select_upto]
Thm* i,j:. ij  upto(i)  upto(j)	[upto_iseg]
Thm* m:, n:(m+1). upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n)))	[upto_decomp]
Thm* n:. upto(n)  n List	[upto_wf]
Thm* f:Top, T:Type, L:T List, i:||L||. map(f;L)[i] ~ (f(L[i]))	[select-map]
Thm* l:T List, i:||l||, j:i. last(l_interval(l;j;i)) = l[(i-1)]	[last_l_interval]
Thm* l:T List, i:||l||, j:i. hd(l_interval(l;j;i)) = l[j]	[hd_l_interval]
Thm* l:T List, i:||l||, j:(i+1), x:(i-j). l_interval(l;j;i)[x] = l[(j+x)]	[select_l_interval]
Thm* l:T List, i:||l||, j:(i+1). ||l_interval(l;j;i)|| = i-j	[length_l_interval]
Def finite-type(T) == n:, f:(nT). Surj(n; T; f)	[finite-type]
Def (x,yL.P(x;y)) == i:||L||, j:i. P(L[j];L[i])	[pairwise]

In prior sections: int 1 bool 1 int 2 list 1 mb basic mb nat mb list 1 num thy 1 mb list 2

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html