Regula rule reference🔗

Regula for Lean is a strict linter: lake lint does not accept a project with a sorry, a project axiom, a compiler-trusting proof such as native_decide, or an axiom beyond the foundation you chose, and names every extern and implemented_by boundary your executables reach. Every rule below has a checked failing example, its fix, and what a pass does and does not establish. New here? Start with what it checks and how to try it.

1. Decide whether to adopt. The rule index lists all 22 rules, and how rules are enforced states what they share: a violation fails the result, and missing evidence never passes. The adoption guide covers installation, lake lint, editor feedback and CI; the standard and its compliance checklist define what the rules enforce; every Lean example of the standard is elaborated when this site is built.

2. Look up a rule. Every finding names a rule ID such as RG1002 (editor code Regula.RG1002) and ends with the URL of its page in the reference of the installed Regula version; the editor's View explanation link opens the same page. A rule page starts with what is wrong, what to do and a checked example. Open the rule index, or press / to search.

3. Review a Regula pass. A finding is a violation, which makes the result FAIL, or incomplete, which makes it INCOMPLETE because required evidence is missing; neither is accepted. A pass is mechanical: each rule page states what the check establishes and which review obligations stay with you, and checklist coverage maps every row of the compliance checklist to the rules that report on it and the review obligations it carries.

4. Challenge a rule. Each rule page gives the rule's rationale, its normative clauses and its detector sources at the commit the page was built from. To dispute a rule or report a wrong result, open an issue.