Commit 2023-01-19 15:23 78314d08

View on Github →

chore(data/fintype/vector, logic/equiv/list): split (#18226) array and d_array do not exist in Lean 4; it's easier for porting if we put the stuff about those types in separate files.

Estimated changes

Modified src/computability/primrec.lean

Modified src/data/array/lemmas.lean

deleted def equiv.array_equiv_fin

deleted def equiv.d_array_equiv_fin

deleted def equiv.vector_equiv_array

Created src/data/fintype/array.lean

Modified src/data/fintype/vector.lean

Created src/logic/equiv/array.lean

added def equiv.array_equiv_fin

added def equiv.d_array_equiv_fin

added def equiv.vector_equiv_array

Modified src/logic/equiv/list.lean