Commit 2024-11-23 06:55 40913713

fix(Tactic/Linter): upstreamableDecl should treat structures like defs (#19360) Reported on Zulip: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/upstreamableDecl.20linter.20bug/near/483790949 We want to treat a structure/inductive declaration in the current file just like a def for the upstreamableDecl linter: potentially place a warning on the structure itself, but otherwise don't place warnings on downstream uses. There's a small complication where inductive declarations are reported to depend on their own constructors. I couldn't find a good way to determine whether any given constant is indeed a constructor declared in some given piece of syntax, so instead we allow depending on constructors just like we allow depending on theorems.