Def dont_propose_to_move_this_def

Modification history

2025-02-04 06:23
MathlibTest/MinImports.lean
feat(Tactic/Linter): options to in/exclude definitions and private decls (#21374) …
Added dont_propose_to_move_this_defView on Github →