Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-08 09:31 ffad43d2

View on Github →

golf(*): λ _, default → default (#14608)

Estimated changes

Modified src/computability/turing_machine.lean

Modified src/data/array/lemmas.lean

Modified src/data/finset/basic.lean

Modified src/data/holor.lean

modified def holor

modified def holor_index

Modified src/data/pfunctor/multivariate/basic.lean

Modified src/data/pfunctor/univariate/M.lean

Modified src/data/pfunctor/univariate/basic.lean

Modified src/data/prod/tprod.lean

Modified src/data/qpf/multivariate/constructions/sigma.lean

Modified src/data/setoid/partition.lean

Modified src/data/vector/basic.lean

Modified src/group_theory/sylow.lean

Modified src/logic/basic.lean

Modified src/logic/embedding.lean

Modified src/logic/equiv/basic.lean

Modified src/logic/unique.lean

Modified src/measure_theory/covering/besicovitch.lean

Modified src/order/jordan_holder.lean

Modified src/order/omega_complete_partial_order.lean

Modified src/topology/continuous_function/basic.lean

Modified src/topology/vector_bundle/basic.lean

Modified test/lint_coe_t.lean

modified def int_to_a