This page documents Regula 0.6.0. The latest release is Regula 0.11.1: this page in Regula 0.11.1.

RG4003: Negative examples require completed intended rejection🔗

Category Documentation
Scope documentation fence
Subreason negative-example

A fence marked lean-fail did not fail as specified: it elaborated successfully, failed for a different reason, or the worker crashed or timed out.

What to do. Make the example fail for exactly the documented reason, adjust the pattern to match one real error message, or remove the marker if the example is valid.

Requirement: A lean-fail fence fails to elaborate with one error message that matches its whole pattern.
Reported in: Docs examples
Enforcement: Strict, like every rule: see how rules are enforced.

Checked example🔗

Violating input

✗ Rejecteddocs/Example.mdsource examples/rules/RG4003/Violation.md

<!-- lean-fail: unknown identifier -->
```lean
/-! # Reflexivity

Reflexivity for every natural number. -/
theorem reflexive (n : Nat) : n = n := rfl
```

Findings of the violating run

RG4003 error violation documentation example

Subject Example.md:2 at project Example.md:2

negative example elaborated successfully

Correction

Change to docs/Example.md

- <!-- lean-fail: unknown identifier -->
  ```lean
  /-! # Reflexivity
  
  ⋯ 3 unchanged lines

✓ Passesdocs/Example.mdsource examples/rules/RG4003/Fixed.md

```lean
/-! # Reflexivity

Reflexivity for every natural number. -/
theorem reflexive (n : Nat) : n = n := rfl
```

The correction labels an already valid reflexivity proof as a positive example instead of inventing a compiler failure.

Checked by a documentation fence audit of <example>/docs: violating run rejected, corrected run completed.

How to fix it🔗

If the example is actually valid, remove the lean-fail marker so it is checked as positive.
If it should fail, edit the example so it fails for the documented reason, and write a pattern that matches that one error message.
Keep patterns to literal fragments joined by .* and alternatives separated by |.

Why it matters🔗

A negative example documents what Lean rejects. If it stops failing, or fails for another reason, the documentation claims a rejection that no longer holds.

What triggers it🔗

A negative fence must complete with a source rejection, and one effective error message must match the entire expected pattern. Informational output, a pattern matched across several messages, a crash, a timeout or a successful elaboration does not pass.

An example that elaborated successfully or failed with a non-matching message is a violation; a worker that crashed, timed out or did not complete is INCOMPLETE.

Required proof shape🔗

The pattern is part of the documented claim and is reviewed with the prose.

What a passing result establishes🔗

The negative fence completed with a source rejection whose single error message matches the whole pattern.

It does not establish:

That the rejection happens for the conceptual reason the prose explains beyond the matched message text.

It leaves these review obligations open: R-QUALIFY, R-DOC.

Configuration and exceptions🔗

The marker and its pattern are the configuration; there is no option that accepts a non-failing negative example.

Limitations and unsupported cases🔗

Regula policy rejections of documentation examples can follow successful elaboration; this rule concerns compiler rejection patterns of lean-fail fences.

Sources🔗

Normative clauses: standard §7.7 Check Lean Documentation Verbatim
Checklist rows: DOC-05
Detector, policy and proof sources: lean/Regula/Checker/Diagnostics.lean, lean/RegulaPolicy/Pattern.lean, lean/Regula/Website.lean
Proved linkage: RegulaPolicy.matchesPattern_iff characterizes the executed matcher.