Rule index🔗

Every rule the linter can emit, generated from its typed registry. The filters work without JavaScript. What every rule shares is on how rules are enforced.

All 24 registered rules
ID	Rule	Category	Reported in
`RG1001`	Project logical axioms are forbiddensubreason `project-axiom`	Foundationdeclaration	EditorProjectSingle fileDocs examples
`RG1002`	Proof holes are forbiddensubreason `hole`	Foundationdeclaration	EditorProjectSingle fileDocs examples
`RG1003`	Unknown transitive axioms are forbiddensubreason `unknown-axiom`	Foundationdeclaration	EditorProjectSingle fileDocs examples
`RG1004`	Compiler-trusting proofs require separate classificationsubreason `compiler-trusting`	Foundationdeclaration	EditorProjectSingle fileDocs examples
`RG1005`	Transitive axioms must fit the selected profilesubreason `label-exceeds-claim`	Foundationdeclaration	EditorProjectSingle file
`RG1006`	Unsafe and partial declarations require exact helper authenticationsubreason `escape-hatch`	Declarationdeclaration	EditorProjectSingle fileDocs examples
`RG1007`	Executable contracts require supported closed evidencesubreason `executable-contract`	Executiondeclaration	EditorProjectSingle fileDocs examples
`RG1008`	Registered decision functions require a decision contractsubreason `decision-contract`	Executiondeclaration	ProjectSingle fileDocs examples
`RG1009`	Decision specifications share no Boolean test with the implementationsubreason `shared-test`	Executiondeclaration	EditorProjectSingle fileDocs examples
`RG2001`	The declared Lean environment must be availablesubreason `environment`	Environmentproject	ProjectSingle file
`RG2002`	Configuration must classify the complete Lake surfacesubreason `configuration`	Configurationproject	EditorProjectSingle file
`RG2003`	Claimed source must elaborate warning-freesubreason `source-build`	Elaborationproject	ProjectSingle file
`RG2004`	Owned coverage must match the exact Lake inventorysubreason `coverage`	Coverageproject	ProjectSingle file
`RG2005`	Required admission and source evidence must be completesubreason `admission`	Admissionproject	EditorProjectSingle fileDocs examples
`RG2006`	Claimed targets must build with the community configurationsubreason `community-configuration`	Configurationproject	Project
`RG3001`	Execution closure must have no unresolved pathssubreason `execution-unresolved`	Executionexecution root	ProjectSingle file
`RG3002`	Checked execution requires admitted correspondencesubreason `execution-trusted-boundary`	Executionexecution root	ProjectSingle file
`RG4001`	Documentation fences must have a valid classificationsubreason `fence-structure`	Documentationdocumentation fence	Docs examples
`RG4002`	Positive examples require warning-free elaboration and admissionsubreason `positive-example`	Documentationdocumentation fence	Docs examples
`RG4003`	Negative examples require completed intended rejectionsubreason `negative-example`	Documentationdocumentation fence	Docs examples
`RG4004`	Teaching examples require authenticated compiler classificationsubreason `trusted-example`	Documentationdocumentation fence	Docs examples
`RG5001`	Claimed modules need a leading module docstring and no repeated importsubreason `module-documentation`	Documentationmodule	EditorProject
`RG5002`	Registered public material declarations require docstringssubreason `material-documentation`	Documentationregistered material declaration	EditorProject
`RG5003`	Registered public material declarations require an Intent sectionsubreason `material-intent`	Documentationregistered material declaration	EditorProject
No registered rule matches the selected filters. Use Reset to show every rule.