Inductive ProposeToMoveThisInductive

Modification history

2024-11-23 06:55

MathlibTest/MinImports.lean

fix(Tactic/Linter): `upstreamableDecl` should treat `structure`s like `def`s (#19360) …

Added ProposeToMoveThisInductive View on Github →