Def def_no_doc'

Modification history

2026-07-18 00:01
MathlibTest/Linter/DocPrime.lean
chore(MathlibTest): fix defLemma warnings (#40593) …
Modified def_no_doc'View on Github →
2024-09-25 13:34
test/DocPrime.lean
feat: the docPrime linter (#16694) …
Added def_no_doc'View on Github →