Commit 2022-04-16 17:33 8decd4b1

View on Github →

chore(logic/encodable/basic): Rename encodable instances (#13396) The instances were called encodable.foo instead of foo.encodable as the naming convention preconizes.

Estimated changes

Modified src/algebra/algebraic_card.lean

Modified src/analysis/box_integral/partition/measure.lean

Modified src/computability/encoding.lean

Modified src/data/W/basic.lean

Modified src/data/rat/denumerable.lean

Modified src/data/set/countable.lean

Modified src/data/tprod.lean

Modified src/logic/encodable/basic.lean

Modified src/logic/equiv/list.lean

deleted def encodable.trunc_encodable_of_fintype

added def fintype.trunc_encodable

Modified src/measure_theory/constructions/borel_space.lean

Modified src/measure_theory/constructions/pi.lean

Modified src/measure_theory/function/strongly_measurable.lean

Modified src/measure_theory/measurable_space.lean

Modified src/measure_theory/measurable_space_def.lean

Modified src/measure_theory/measure/hausdorff.lean

Modified src/measure_theory/measure/measure_space.lean

Modified src/model_theory/basic.lean

Modified src/model_theory/encoding.lean

Modified src/set_theory/cardinal_ordinal.lean

Modified src/topology/bases.lean

Modified src/topology/metric_space/basic.lean