Zulip Chat Archive

Stream: mathlib4

Topic: linting

Patrick Massot (Oct 18 2022 at 20:28):

Should we have a mathlib4 root file containing

import Std.Tactic.Lint.Frontend
import Std.Tactic.Lint.Misc

What about

import Mathlib.Mathport.Rename

Patrick Massot (Oct 18 2022 at 20:42):

By the way, I just added information from this thread at https://github.com/leanprover-community/mathlib4/wiki/Home/_compare/d4174b6f13a7d952fd05084f032eba0bb4550a00...216499acb1561b28c9f0eb274b26671016c01baf

Last updated: Dec 20 2023 at 11:08 UTC