Regula rule reference
Regula. A strict linter for Lean. It checks that each theorem of the libraries that you claim depends only on the axioms of the foundation that you choose, also through imports. Thus lake lint refuses a sorry, an axiom of those libraries and native_decide, which lake build accepts. This site is the reference of the Regula edition above: a page for each rule, and the standard that the rules come from. New here? Try it on one module, then add it to your project.
-
Look up a rule. Each finding names a rule ID. In the terminal, the first finding of each rule in a run links the page of the rule, and later findings of that rule refer to it. The editor and the JSON report link the page with each finding. A rule page starts with the problem, the fix and an example that the checker rejects. Open the rule index, or push
/to search. -
Adopt Regula. The adoption guide tells how to install and run Regula, in the terminal, in the editor and in CI.
-
Review a pass. A pass is mechanical. Each rule page tells what the check shows and which review stays with you. How rules are enforced and checklist coverage give the details.
-
Challenge a rule. Each rule page gives the reason for the rule, its clauses in the standard and the source of its check. To dispute a rule, open an issue.