Commit 2021-11-22 15:44 c8520c4a

View on Github →

feat: add simp linter (#100) Still requires a bit more testing.

  1. Lean now has a built-in feature called "linter" which is something different, I've tried to use mathlibLinter for the attribute.
  2. I haven't checked that nolint works yet.
  3. The simp linter is still a bit buggy (reports "can be replace by by simp only []" way too often)
  4. Detecting automatically generated declarations is a todo.
  5. CI integration with nolints.txt is missing.
  6. Other linters are also missing.

Estimated changes

modified theorem neg_eq_of_add_eq_zero
modified theorem equiv.coe_fn_mk
modified theorem List.length_singleton
modified theorem List.mem_cons
modified theorem List.mem_insert_self
modified theorem List.mem_nil
modified theorem List.mem_nil_iff
modified theorem List.mem_singleton
modified theorem List.not_mem_nil
added theorem List.repeatSucc
deleted def List.repeatSucc
modified theorem List.singleton_append
modified theorem Prod.map_mk
modified theorem Prod.mk.inj_iff
modified theorem Prod.swap_left_inverse
modified theorem Prod.swap_right_inverse
modified theorem prod_map
modified theorem String.congr_append
modified theorem Subtype.coe_mk
modified theorem Subtype.val_prop
deleted theorem Nat.nat_zero_eq_zero
modified theorem Ne.def
modified theorem eq_self_iff_true
modified theorem not_false_iff
modified theorem not_true
modified theorem opt_param_eq
modified theorem Function.const_apply
added def Option.mapM