Commit 2025-02-04 06:23 02696de6

View on Github →

feat(Tactic/Linter): options to in/exclude definitions and private decls (#21374) Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/late.20imports Two new options:

linter.upstreamableDecl.defs (default: false): warn if a definition can be upstreamed
linter.upstreamableDecl.private (default: false): warn if a private declaration can be upstreamed

Estimated changes

Modified Mathlib/Tactic/Linter/UpstreamableDecl.lean

Modified MathlibTest/MinImports.lean

added inductive DontProposeToMoveThisInductive

added structure DontProposeToMoveThisStructure

deleted def def_with_multiple_dependencies

added def dont_propose_to_move_this_def

added theorem theorem_with_multiple_dependencies