Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-01 21:07 4274dddf

View on Github →

chore(*): bump to Lean 3.18.4 (#3610)

Remove pi_arity and the vm_override for by_cases, which have moved to core
Fix fallout from the change to the definition of max
Fix a small number of errors caused by changes to instance caching
Remove min_add, which is generalized by min_add_add_right and make to_additive generate some lemmas

Estimated changes

Modified leanpkg.toml

Modified src/algebra/order_functions.lean

deleted theorem fn_min_add_fn_max

deleted theorem min_add

deleted theorem min_add_max

Modified src/algebra/ordered_group.lean

Modified src/computability/primrec.lean

modified theorem primrec.nat_max

Modified src/control/traversable/equiv.lean

Modified src/data/int/cast.lean

Modified src/data/list/min_max.lean

Modified src/data/polynomial/monic.lean

Modified src/data/rat/cast.lean

Modified src/measure_theory/borel_space.lean

Modified src/meta/expr.lean

Modified src/order/filter/filter_product.lean

Modified src/ring_theory/algebra_tower.lean

Modified src/set_theory/ordinal.lean

Modified src/tactic/core.lean

Deleted src/tactic/fix_by_cases.lean

Modified src/tactic/interval_cases.lean

Modified src/topology/algebra/ordered.lean