Checked example🔗

/-! # Identity

Identity on natural numbers. -/
/-- The identity function on natural numbers. -/
def identity (n : Nat) : Nat := (fun unused : Nat => n) 0

<example>/.lake/regula-scratch/file-audit-4934-368654254325-16279956453913272568/AuditFile_364707025089.lean:5:37: warning: Variable name `unused` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _unused

Note: This linter can be disabled with `set_option linter.unusedVariables false`

  /-! # Identity
  
  Identity on natural numbers. -/
  /-- The identity function on natural numbers. -/
- def identity (n : Nat) : Nat := (fun unused : Nat => n) 0
+ def identity (n : Nat) : Nat := n

/-! # Identity

Identity on natural numbers. -/
/-- The identity function on natural numbers. -/
def identity (n : Nat) : Nat := n

The correction removes a dead lambda binding while preserving identity's complete natural-number behavior. No warning or linter is disabled.

Checked by a fresh single-file audit of <example>/Fixture.lean (axiomGate --file, claim kernel-only, execution checked): violating run rejected, corrected run completed.

How to fix it🔗

1. Read the preserved compiler message, fix the cause and rebuild.

2. Remove dead bindings or rename intentionally unused ones only when the name was genuinely unused; do not rename a variable that should have been used.

3. Do not add set_option linter.… false for a Lean default warning such as linter.unusedVariables. A declaration-scoped set_option linter.NAME false in or @[nolint NAME] is only for a community linter, enabled by a dependency or the project, where its guidance allows, and establishes nothing the linter checks.

Why it matters🔗

Warnings often mark real defects (unused hypotheses, deprecated semantics, unreachable cases). Treating them as failures keeps the elaborated statements exactly those the author intended, and prevents a local option from changing what conformance means.

What triggers it🔗

The audit builds the claimed targets itself and checks both the exit status and every emitted diagnostic. Any warning fails, including when the source sets warningAsError to false locally (for a single-file audit, when any --claim is requested). The original compiler message is preserved in the finding.

In project runs (lake lint, axiomGate, the build-lint policy target) a warning or failed build stops the audit before policy inspection, so the finding is incomplete and the result INCOMPLETE (lake lint exit 3). A single-file axiomGate --file F --claim P audit reports a completed source rejection as a violation, as in the checked example; without --claim warnings do not fail a file audit (an elaboration error is still a RG2003 violation), a file that elaborates and passes the declaration rules is CLASSIFIED rather than accepted, and a failed build of the manifest's claimed targets it depends on is INCOMPLETE.

Required proof shape🔗

The fix must not change the proposition or behavior being claimed; if it does, review the statement again.

What a passing result establishes🔗

Every claimed module elaborated from source without errors or warnings under the audit's build.

It does not establish:

• Fresh source elaboration unless the run is fresh: lake lint without --fresh is incremental and trusts Lake's build cache.

• That no linter was disabled: a disabled linter emits nothing for this rule to reject.

It leaves these review obligations open: R-QUALIFY.

Configuration and exceptions🔗

warningAsError := false in the source cannot hide a warning from the audit. Disabling a linter stops it from emitting, which makes this rule pass without establishing the property the linter checks. Never disable Lean's default warnings, such as linter.unusedVariables (for example with set_option linter.unusedVariables false).

A community linter reports through build warnings, so this rule rejects its findings, whether a dependency turns it on for every importer (such as Mathlib's linter.unusedTactic) or the project enables it (such as linter.missingDocs and Mathlib's weak.linter.mathlibStandardSet, which standard §6.7 requires). Where the community's guidance allows an exception, disable that linter for one declaration (set_option linter.NAME false in or @[nolint NAME]) with a comment giving the reason (standard §6.2). The detector sees only emitted warnings, so it cannot tell such a disable from a forbidden one; review checks them.

Limitations and unsupported cases🔗

lake lint builds with Regula's audit-build marker, which turns the local linter off whatever the source sets linter.regula to, so Regula's own local findings are not build warnings there and its policy stages report those rules. axiomGate and the build-lint policy target keep ordinary options, so in a module that imports Regula.Linter a local Regula finding is a build warning and makes the result INCOMPLETE under this rule.

Sources🔗

Normative clauses

standard §7.3 Clean Elaboration and Diagnostics

Checklist rows

DECL-01, BUILD-01, DOC-01

Detector, policy and proof sources

lean/Regula/Checker/Lake.lean, lean/Regula/Checker/Diagnostics.lean, lean/Regula/Checker/ResultProtocol.lean

Proved linkage

Acceptance side only: an accepted run satisfies RegulaPolicy.BuildOK. Reading Lake's build result is operational.