Thm* Q:((T List)Prop).
Thm* Q(nil)
Thm*
Thm* (x:T. Q([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:C, as:A List, g:(A(A List)B).
Thm* (ForHdTl{A,f,k} h::t as. g(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:B, as: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:T, as:T List, i:. 0<i i||as|| (a.as)\[i] = a.as\[i-1] | [reject_cons_tl] |
Thm* a:T, as:T List, i:. i0 (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:T, as:T List, i:. 0<i i||as|| (a.as)[i] = as[(i-1)] | [select_cons_tl] |
Thm* a:T, as:T List, i:. i0 (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:A, as,bs:A List. a.as = b.bs a = b | [eq_cons_imp_eq_hds] |
Thm* a,b:A, as,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||1 ||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||1 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:A, as: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:T, t:T List. h.t = nil | [cons_neq_nil] |