Def propose_to_move_this_def

Modification history

2024-11-18 11:19
MathlibTest/MinImports.lean
feat: the upstreamDecl linter (#18702) …
Added propose_to_move_this_defView on Github →