Structure DontProposeToMoveThisStructure

Modification history

2025-02-04 06:23

MathlibTest/MinImports.lean

feat(Tactic/Linter): options to in/exclude definitions and private decls (#21374) …

Added DontProposeToMoveThisStructure View on Github →