opaque Lean.backward.defeqAttrib.useBackward : Lean.Option Bool

def Lean.validateDefEqAttr (declName : Name) : AttrM Unit

Validates that declName is a definitional equality at .default/.all transparency (the legacy permissive check). Throws a diagnostic error if not. This is used both as the validator for the @[defeq] and @[backward_defeq] attributes and as a building block for inferDefEqAttr.

Equations

• One or more equations did not get rendered due to their size.

opaque Lean.backwardDefeqAttr : TagAttribute

Marks a theorem as a definitional equality under the permissive transparency rules that predated the stricter @[defeq] inference (i.e. an equality that holds at .default or .all transparency, but possibly not at .instances transparency as required by dsimp).

Such theorems are inferred automatically by inferDefEqAttr: any theorem that the old := rfl inference would have accepted is tagged @[backward_defeq], and additionally tagged @[defeq] when it also passes the stricter check at instance transparency.

dsimp ignores @[backward_defeq] theorems by default. Setting set_option backward.defeqAttrib.useBackward true (typically scoped to a single proof with set_option ... in) makes dsimp treat them like @[defeq] theorems, which provides a local backwards-compatibility escape hatch for proofs broken by the stricter inference.

opaque Lean.defeqAttr : TagAttribute

Marks the theorem as a definitional equality that can be used by dsimp.

The theorem must be an equality that holds at .instances transparency. A theorem with a definition that is (syntactically) := rfl is implicitly marked @[defeq] (and also @[backward_defeq], since the latter is a superset); write := (rfl) instead to suppress this.

The attribute should be given before a @[simp] attribute to have effect.

When using the module system, an exported theorem can only be @[defeq] if all definitions that need to be unfolded to prove the theorem are exported and exposed.

Tagging a theorem with @[defeq] automatically also tags it with @[backward_defeq], maintaining the invariant that @[defeq] theorems form a subset of @[backward_defeq] theorems.

def Lean.inferDefEqAttr (declName : Name) : MetaM Unit

For automatically generated theorems (equational theorems etc.), we tag the theorem with the defeq/backward_defeq attributes based on its rfl proof:

• If the equation holds at .instances transparency (matching the transparency at which dsimp operates), we tag it with @[defeq].
• Independently, if the equation holds under the more permissive legacy check (equivalent to validateDefEqAttr, i.e. at .default or .all transparency), we tag it with @[backward_defeq].

In particular, every theorem that would have been tagged @[defeq] before the stricter inference rules were introduced is now tagged @[backward_defeq]. Local backwards compatibility can be restored with set_option backward.defeqAttrib.useBackward true.

Equations

• One or more equations did not get rendered due to their size.