Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-02 19:25 d3b8622b

View on Github →

fix(tactic/lint): simp_nf: do not ignore errors (#2266) This PR fixes some bugs in the simp_nf linter. Previously it ignored all errors (from failing tactics). I've changed this so that errors from linters are handled centrally and reported as linter warnings. The simp_is_conditional function was also broken. As usual, new linters find new issues:

Apparently Lean sometimes throws away simp lemmas. https://github.com/leanprover-community/lean/issues/163
Some types define has_coe but have an incorrect has_coe_to_fun, causing the simplifier to loop ⇑f a = ⇑↑f a = ⇑f a. See the new library note:

Estimated changes

Modified src/algebra/field.lean

modified theorem is_ring_hom.map_eq_zero

modified theorem is_ring_hom.map_ne_zero

Modified src/category_theory/monoidal/functorial.lean

Modified src/data/indicator_function.lean

modified theorem set.indicator_apply

Modified src/data/set/basic.lean

modified theorem set.ne_empty_iff_nonempty

Modified src/linear_algebra/basic.lean

Modified src/logic/basic.lean

Modified src/order/order_iso.lean

modified theorem order_iso.coe_coe_fn

Modified src/set_theory/ordinal.lean

deleted theorem initial_seg.of_iso_apply

Modified src/tactic/core.lean

Modified src/tactic/lint.lean

Modified src/topology/algebra/module.lean

Modified src/topology/basic.lean

deleted theorem subsingleton.is_closed

deleted theorem subsingleton.is_open

Modified src/topology/order.lean

added theorem is_closed_discrete