Module equations 

Equation lemmas — Lean’s f.eq_def, f.eq_1 … f.eq_n — the NAME a proof cites when it appeals to a definition’s behaviour, which is what rw [f] / simp [f] / unfold f all need.

A LOGOS definition is δ-transparent and its Fix/Match ι-compute, so the facts about a recursive function are all TRUE by conversion the moment it is declared: dbl 3 ≡ 6, and dbl (Succ n) ≡ Succ (Succ (dbl n)) for a free n. What was missing is a name. Every appeal to a definition in a real proof — rw [f], simp [f], unfold f — cites a CONSTANT, and without one every such appeal degrades to a full normalize whose fuel silently returns a partially reduced term when it runs out.

What Lean does, and where

• The names. Lean/Meta/Eqns.lean:59-68 fixes them: eqnThmSuffixBase := "eq", eqn1ThmSuffix := "eq_1", unfoldThmSuffix := "eq_def". In Lean’s hierarchical namespace those are f.eq_def and f.eq_1 … f.eq_n; LOGOS’s context is flat, so the same suffixes are spelled f_eq_def and f_eq_1 … f_eq_n.
• The shape and the proof. Lean/Meta/Eqns.lean:149-162 (mkSimpleEqThm) telescopes the definition’s VALUE, states ∀ xs, f xs = body, and proves it with Eq.refl (f xs) under the same telescope. That is exactly the shape built here: the theorem is true by conversion, so refl is the whole proof, and the kernel’s own registration gateway re-checks it.
• When. Lean/Meta/Eqns.lean:142-144 — “We generate the equations on demand” — via getEqnsFor? and the reserved-name action at Lean/Meta/Eqns.lean:281-289. LOGOS generates EAGERLY instead, and the reason is a signature rather than a preference: Context::get_global returns Option<&Term>, a reference into the context, so a lookup cannot synthesise a term it does not already hold. Eager generation costs one refl per definition and makes the lemma visible to every reader, including Check.

The three hazards, and how each is closed

• Re-entrancy. A lemma is itself a definition, so generating one would generate its own. is_equation_name is checked first and an equation name generates nothing.
• Bootstrap. Eq and refl are registered part-way through the prelude (prelude.rs::register_eq), so everything declared before them has no equality to state an equation IN. Generation is a no-op while they are absent, and generate_missing_for_all back-fills once they exist.
• Displacement. Context::declare displaces the name it registers. A lemma is skipped whenever its name is already taken, so generation can never remove something a user wrote.

Constants

EQUATION_INFIX

Lean’s eqnThmSuffixBasePrefix (Lean/Meta/Eqns.lean:60), flattened.

UNFOLD_SUFFIX

Lean’s unfoldThmSuffix (Lean/Meta/Eqns.lean:68), flattened.

Functions

equation_lemmas

The equation lemmas a definition owes, as (name, statement, proof) in Lean’s order: the unfold theorem first, then one equation per constructor of the matched argument.

generate

Generate and REGISTER the equation lemmas a definition owes.

generate_missing_for_all

Back-fill every definition that was registered before Eq/refl existed.

is_equation_name

Whether a name is one this module MINTS, rather than one it generates lemmas for.