Defs

📁 Source: Mathlib/Data/Vector/Defs.lean

Statistics

Metric	Count
Definitions cons, drop, elim, eraseIdx, get, head, instDecidableEq, instGetElemNatLt, instHAppendHAddNat, length, map, mapAccumr, mapAccumr₂, map₂, nil, ofFn, pmap, replicate, shiftLeftFill, shiftRightFill, tail, take, toList	23
Theorems append_def, cons_head_tail, eq, eq_nil, getElem_def, head_cons, map_cons, map_nil, pmap_nil, tail_cons, toList_append, toList_cons, toList_drop, toList_getElem, toList_length, toList_mk, toList_nil, toList_take	18
Total	41

List.Vector

Definitions

Name	Category	Theorems
cons 📖	CompOp	45 math math: Computable.vector_cons, scanl_nil, tail_cons, get_cons_nil, map_cons, cons_val, mmap_cons, eq_cons_iff, replicate_succ, traverse_def, Equiv.Perm.VectorsProdEqOne.vectorEquiv_apply_coe, get_cons_zero, Nat.Partrec'.map, get_append_cons_zero, exists_eq_cons, Nat.Primrec'.prec', tendsto_cons, reverse_cons, inductionOn_cons, mem_cons_self, mem_cons_iff, mapAccumr₂_cons, mapAccumr_cons, toList_cons, scanl_singleton, pmap_cons, Equiv.Perm.VectorsProdEqOne.one_eq, Nat.Primrec'.cons, Nat.Partrec'.bind, cons_head_tail, head_cons, Primrec.vector_cons, Nat.Partrec'.cons, get_append_cons_succ, map₂_cons, get_cons_succ, scanl_cons, snoc_nil, mem_cons_of_mem, Sym.cons_of_coe_eq, Nat.Partrec'.rfindOpt, Sym.ofVector_cons, pmap_cons', snoc_cons, reverse_snoc
drop 📖	CompOp	3 math math: sum_set, prod_set, toList_drop
elim 📖	CompOp	—
eraseIdx 📖	CompOp	5 math math: continuousAt_eraseIdx, continuous_eraseIdx, eraseIdx_val, eraseIdx_insertIdx', eraseIdx_insertIdx_self
get 📖	CompOp	30 math math: scanl_get, last_def, get_cons_nil, get_tail_succ, get_mem, get_cons_zero, get_eq_get_toList, mem_iff_get, ofFn_get, get_append_cons_zero, get_tail, zipWith_get, nodup_iff_injective_get, get_set_same, ext_iff, Primrec.vector_get, sum_set', get_ofFn, get_replicate, prod_set', get_append_cons_succ, get_set_eq_if, Primrec.vector_get', get_cons_succ, Computable.vector_get, get_zero, get_set_of_ne, get_map, get_map₂, Fin.card_filter_univ_eq_vector_get_eq_count
head 📖	CompOp	29 math math: Nat.Primrec'.sub, eq_cons_iff, head_mem, Nat.Primrec'.natPair, head?_toList, Nat.Primrec'.pred, Nat.Primrec'.head, mem_map_succ_iff, Nat.Primrec'.prim_iff₂, scanl_head, scanl_singleton, Nat.Primrec'.add, Computable.vector_head, cons_head_tail, Nat.Partrec'.part_iff₂, head_cons, toList_singleton, Nat.Primrec'.prim_iff₁, reverse_get_zero, head_ofFn, Nat.Partrec'.head, get_zero, Nat.Primrec'.mul, Nat.Primrec'.sqrt, head_map, Nat.Partrec'.part_iff₁, mem_succ_iff, head_pmap, Primrec.vector_head
instDecidableEq 📖	CompOp	—
instGetElemNatLt 📖	CompOp	4 math math: getElem_def, toList_getElem, getElem_pmap, getElem_map
instHAppendHAddNat 📖	CompOp	5 math math: get_append_cons_zero, append_def, append_nil, get_append_cons_succ, toList_append
length 📖	CompOp	2 math math: Computable.vector_length, Primrec.vector_length
map 📖	CompOp	25 math math: map_map, map_cons, mem_map_iff, map₂_map_left, map_mapAccumr, mapAccumr_eq_map_of_constant_state, mem_map_succ_iff, traverse_eq_map_id, map_map₂, toList_map, map_eq_mapAccumr, mapAccumr_eq_map_of_unused_state, map_pmap, getElem_map, mapAccumr_eq_map, map_nil, pmap_map, map_snoc, mapAccumr_map, map₂_map_right, get_map, head_map, tail_map, notMem_map_zero, map_id
mapAccumr 📖	CompOp	18 math math: mapAccumr_snoc, mapAccumr₂_mapAccumr_left, map_mapAccumr, mapAccumr_eq_map_of_constant_state, mapAccumr_nil, mapAccumr₂_mapAccumr_right, mapAccumr_cons, mapAccumr_bisim_tail, map_eq_mapAccumr, mapAccumr_eq_map_of_unused_state, mapAccumr_eq_map, mapAccumr_map, mapAccumr_mapAccumr, mapAccumr₂_unused_input_right, mapAccumr_redundant_pair, mapAccumr_bisim, mapAccumr₂_unused_input_left, mapAccumr_mapAccumr₂
mapAccumr₂ 📖	CompOp	21 math math: mapAccumr₂_mapAccumr_left, mapAccumr₂_nil, mapAccumr₂_mapAccumr₂_left_right, mapAccumr₂_snoc, mapAccumr₂_eq_map₂_of_unused_state, mapAccumr₂_bisim, mapAccumr₂_mapAccumr_right, mapAccumr₂_comm, mapAccumr₂_cons, mapAccumr₂_eq_map₂_of_constant_state, mapAccumr₂_eq_map₂, mapAccumr₂_flip, mapAccumr₂_unused_input_right, mapAccumr₂_mapAccumr₂_right_left, mapAccumr₂_mapAccumr₂_left_left, mapAccumr₂_redundant_pair, mapAccumr₂_mapAccumr₂_right_right, mapAccumr₂_unused_input_left, mapAccumr₂_bisim_tail, mapAccumr_mapAccumr₂, map₂_eq_mapAccumr₂
map₂ 📖	CompOp	13 math math: map₂_map_left, mapAccumr₂_eq_map₂_of_unused_state, map₂_snoc, map_map₂, map₂_nil, map₂_comm, mapAccumr₂_eq_map₂_of_constant_state, map₂_flip, map₂_map_right, mapAccumr₂_eq_map₂, map₂_cons, get_map₂, map₂_eq_mapAccumr₂
nil 📖	CompOp	22 math math: scanl_nil, get_cons_nil, mapAccumr₂_nil, Equiv.Perm.VectorsProdEqOne.zero_eq, eq_nil, mapAccumr_nil, Sym.ofVector_nil, map₂_nil, Nat.Partrec'.nil, scanl_singleton, append_nil, Equiv.Perm.VectorsProdEqOne.one_eq, toList_nil, mmap_nil, map_nil, tail_nil, Nat.Primrec'.nil, notMem_nil, inductionOn_nil, snoc_nil, pmap_nil, singleton_tail
ofFn 📖	CompOp	11 math math: mOfFn_pure, ofFn_get, tail_ofFn, Primrec.vector_ofFn', toList_ofFn, Vector.mOfFn_part_some, Computable.vector_ofFn', Computable.vector_ofFn, get_ofFn, Primrec.vector_ofFn, head_ofFn
pmap 📖	CompOp	9 math math: getElem_pmap, pmap_cons, map_pmap, pmap_map, toList_pmap, pmap_nil, head_pmap, tail_pmap, pmap_cons'
replicate 📖	CompOp	4 math math: replicate_succ, replicate_succ_to_snoc, Turing.TM1to1.exists_enc_dec, get_replicate
shiftLeftFill 📖	CompOp	—
shiftRightFill 📖	CompOp	—
tail 📖	CompOp	26 math math: Nat.Primrec'.sub, tail_cons, get_tail_succ, eq_cons_iff, Nat.Primrec'.natPair, mem_map_succ_iff, tail_ofFn, Nat.Primrec'.prim_iff₂, get_tail, Nat.Partrec'.tail, Primrec.vector_tail, zipWith_tail, Nat.Primrec'.add, cons_head_tail, Nat.Partrec'.part_iff₂, tail_nil, Equiv.Perm.VectorsProdEqOne.vectorEquiv_symm_apply, Nat.Primrec'.tail, Nat.Primrec'.mul, tail_val, tail_map, toList_tail, Computable.vector_tail, mem_succ_iff, tail_pmap, singleton_tail
take 📖	CompOp	3 math math: sum_set, prod_set, toList_take
toList 📖	CompOp	48 math math: Primrec.vector_toList_iff, toList_mk, mem_map_iff, getElem_def, Turing.TM1to1.stepAux_write, head_mem, get_mem, head?_toList, Equiv.Perm.VectorsProdEqOne.vectorEquiv_apply_coe, get_eq_get_toList, mem_iff_get, not_empty_toList, mem_map_succ_iff, notMem_zero, mem_cons_self, sum_set, toList_map, mem_cons_iff, nodup_iff_injective_get, Equiv.Perm.VectorsProdEqOne.mem_iff, toList_ofFn, toList_cons, toList_length, prod_set, sum_set', toList_empty, toList_nil, toList_singleton, Primrec.vector_toList, toList_set, prod_set', Computable.vector_toList, toList_injective, notMem_nil, toList_scanl, toList_take, toList_append, toList_pmap, toList_reverse, empty_toList_eq_ff, zipWith_toList, Fin.card_filter_univ_eq_vector_get_eq_count, notMem_map_zero, sum_add_sum_eq_sum_zipWith, toList_tail, mem_succ_iff, toList_drop, prod_mul_prod_eq_prod_zipWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
append_def 📖	mathematical	—	List.Vector instHAppendHAddNat	—	—
cons_head_tail 📖	mathematical	—	cons head tail	—	—
eq 📖	—	toList	—	—	—
eq_nil 📖	mathematical	—	nil	—	eq
getElem_def 📖	mathematical	—	List.Vector instGetElemNatLt toList	—	—
head_cons 📖	mathematical	—	head cons	—	—
map_cons 📖	mathematical	—	map cons	—	—
map_nil 📖	mathematical	—	map nil	—	—
pmap_nil 📖	mathematical	—	pmap nil	—	—
tail_cons 📖	mathematical	—	tail cons	—	—
toList_append 📖	mathematical	—	toList List.Vector instHAppendHAddNat	—	—
toList_cons 📖	mathematical	—	toList cons	—	—
toList_drop 📖	mathematical	—	toList drop	—	—
toList_getElem 📖	mathematical	toList	List.Vector instGetElemNatLt	—	—
toList_length 📖	mathematical	—	toList	—	—
toList_mk 📖	mathematical	—	toList	—	—
toList_nil 📖	mathematical	—	toList nil	—	—
toList_take 📖	mathematical	—	toList take	—	—

---

← Back to Index