list 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def x:AB(x) == x:AB(x)

is mentioned by

Thm* Q:((T List)Prop). 
Thm* Q(nil)
Thm* 
Thm* (x:TQ([x]))
Thm* 
Thm* (ys,ys':T List. Q(ys Q(ys' Q(ys @ ys'))  (zs:T List. Q(zs))
[list_append_ind]
Thm* A,B:Type, f:(AB). mapc(f (A List)(B List)[mapc_wf]
Thm* n:as:A List(n). ||as|| = n[list_n_properties]
Thm* n:f:(nT), i:n. (f{n})[i] = f(i)[select_listify_id]
Thm* as:T List. (i:||as||. as[i]){||as||} = as[listify_select_id]
Thm* m,n:f:({m..n}T). n<m  ||f{m..n}|| = n-m[listify_length]
Thm* T:Type, m,n:f:({m..n}T). f{m..n T List[listify_wf]
Thm* A,B,C:Type, f:(BCC), k:Cas:A List, g:(A(A List)B).
Thm* (ForHdTl{A,f,kh::t  asg(h,t))  C
[for_hdtl_wf]
Thm* A,B:Type, f:(A(A List)B), l:A List. mapcons(f;l B List[mapcons_wf]
Thm* A,B:Type, f:(ABB), k:Bas:A List. reduce(f;k;as B[reduce_wf]
Thm* f:(AB), as:A List, n:||as||. map(f;as)[n] = f(as[n])[map_select]
Thm* a:Tas:T List, i:. 0<i  i||as||  (a.as)\[i] = a.as\[i-1][reject_cons_tl]
Thm* a:Tas:T List, i:i (a.as)\[i] = as[reject_cons_hd]
Thm* A:Type, l:A List, n:l\[n A List[reject_wf]
Thm* as:T List, n:{0...||as||}, i:n. firstn(n;as)[i] = as[i][select_firstn]
Thm* as:T List, n:{0...||as||}, i:(||as||-n). nth_tl(n;as)[i] = as[(i+n)][select_nth_tl]
Thm* as:A List, n:(||as||-1). tl(as)[n] = as[(n+1)][select_tl]
Thm* as,bs:T List, i:||as||. (as @ bs)[i] = as[i][select_append_front]
Thm* as,bs:T List, i:{||as||..(||as||+||bs||)}. (as @ bs)[i] = bs[(i-||as||)][select_append_back]
Thm* a:Tas:T List, i:. 0<i  i||as||  (a.as)[i] = as[(i-1)][select_cons_tl]
Thm* a:Tas:T List, i:i (a.as)[i] = a[select_cons_hd]
Thm* A:Type, l:A List, n:. 0n  n<||l||  l[n A[select_wf]
Thm* a,b:Aas,bs:A List. a.as = b.bs  a = b[eq_cons_imp_eq_hds]
Thm* a,b:Aas,bs:A List. a.as = b.bs  as = bs[eq_cons_imp_eq_tls]
Thm* as:T List, i:{0...||as||}, j:{i...||as||}. ||as[i..j]|| = j-i[length_segment]
Thm* as:A List, n:{0...||as||}. ||firstn(n;as)|| = n[length_firstn]
Thm* A:Type, as:A List, n:. firstn(n;as A List[firstn_wf]
Thm* as,bs:T List. rev(as @ bs) = (rev(bs) @ rev(as))[reverse_append]
Thm* T:Type, as:T List. rev(as T List[reverse_wf]
Thm* as:A List, n:{0...||as||}. ||nth_tl(n;as)|| = ||as||-n[length_nth_tl]
Thm* A:Type, as:A List, i:. nth_tl(i;as A List[nth_tl_wf]
Thm* l:A List. ||l|| ||tl(l)|| = ||l||-1[length_tl]
Thm* A:Type, l:A List. tl(l A List[tl_wf]
Thm* A:Type, l:A List. ||l|| hd(l A[hd_wf]
Thm* as:A List. map(Id;as) = as[map_id]
Thm* f:(AB), as,as':A List. map(f;as @ as') = (map(f;as) @ map(f;as'))[map_append]
Thm* f:(AB), g:(BC), as:A List. map(g;map(f;as)) = map(g o f;as)[map_map]
Thm* f:(AB), as:A List. ||map(f;as)|| = ||as||[map_length]
Thm* A,B:Type, f:(AB), l:A List. map(f;l B List[map_wf]
Thm* as:A List. as = nil  ||as|| = 0[length_of_null_list]
Thm* as:A List. as = nil  ||as||1[length_of_not_nil]
Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs||[length_append]
Thm* l:A List. l = nil  ||l||1[pos_length]
Thm* l:A List. ||l||0[non_neg_length]
Thm* a:Aas:A List. ||a.as|| = ||as||+1[length_cons]
Thm* A:Type, l:A List. ||l||  [length_wf1]
Thm* as:T List. (as @ nil) = as[append_back_nil]
Thm* as,bs,cs:T List. ((as @ bs) @ cs) = (as @ (bs @ cs))[append_assoc]
Thm* T:Type, as,bs:T List. (as @ bs T List[append_wf]
Thm* as:T List. null(as as = nil[assert_of_null]
Thm* T:Type, as:T List. null(as [null_wf]
Thm* h:Tt:T List. h.t = nil[cons_neq_nil]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2

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

list 1 Sections StandardLIB Doc