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

Equations

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

opaque Lean.defeqAttr : TagAttribute

Marks the theorem as a definitional equality.

The theorem must be an equality that holds by rfl. This allows dsimp to use this theorem when rewriting.

A theorem with with a definition that is (syntactically) := rfl is implicitly marked @[defeq]. To avoid this behavior, write := (rfl) instead.

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.

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

For automatically generated theorems (equational theorems etc.), we want to set the defeq attribute if the proof is rfl, essentially reproducing the behavior before the introduction of the defeq attribute. This function infers the defeq attribute based on the declaration value.

Equations

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