mathlib
173e70a0 - feat(tactic/lint): rename and refactor sanity_check (#1556)

Commit
6 years ago
feat(tactic/lint): rename and refactor sanity_check (#1556) * chore(*): rename sanity_check to lint * rename sanity_check files to lint * refactor(tactic/lint): use attributes to add new linters * feat(tactic/lint): restrict which linters are run * doc(tactic/lint): document * doc(tactic/lint): document list_linters * chore(tactic/doc_blame): turn doc_blame into a linter * remove doc_blame import * fix(test/lint) * feat(meta/rb_map): add name_set.insert_list * feat(tactic/lint): better control over which linters are run * ignore instances in doc_blame * update lint documentation * minor refactor * correct docs * correct command doc strings * doc rb_map.lean * consistently use key/value * fix command doc strings
Author
Committer
Parents
Loading