unknown constant (after rename) 補題名がバージョン間で変更されている

Error message

unknown constant 'Nat.succ_eq_add_one'

A named lemma or definition existed in an earlier Lean 4 or Mathlib release under one name and now lives under a different one — or was split, merged, or removed. Lean does not automatically forward old names to new ones.

Minimal reproduction

-- File: OldName.lean
example (n : Nat) : n.succ = n + 1 :=
  Nat.succ_eq_add_one n     -- unknown constant in some toolchains
OldName.lean:2:2: error: unknown constant 'Nat.succ_eq_add_one'

The specific name shown here is illustrative — the same class of error surfaces whenever a stdlib or Mathlib identifier moves. Common causes:

Fix

Step 1 — pin the toolchain. LeanDFumt pins lean-toolchain:

leanprover/lean4:v4.27.0

Any downstream project embedding LeanDFumt should either match this version or explicitly test against a newer one before upgrading. The toolchain file is the single source of truth.

Step 2 — locate the current name. From a Lean file in the target toolchain, use #find or the language server's "go to definition":

example (n : Nat) : n.succ = n + 1 := by
  exact?      -- suggests the current lemma name
  -- or:
  #find (?n : Nat).succ = ?n + 1

Step 3 — replace, or derive. Prefer replacing with the current name. If the lemma no longer exists as a named result but is provable by a short tactic, derive it inline — this insulates future toolchain bumps from another rename:

example (n : Nat) : n.succ = n + 1 := rfl

For LeanDFumt itself the risk is minimal — the library depends only on Lean core, and all 29 theorems are decide-proved rather than name-referenced. Downstream projects that call into LeanDFumt should nonetheless watch lean-toolchain when consuming a new tag.

Detection: CHECKER_SPEC

v0 primitive (available today — spec §4, Appendix A): Lean rejects the file with unknown constant '…' and no VERDICT line is emitted. verify() returns UNDECIDED / MISSING_AXIOM — the reason code for "a required constant, axiom, or lemma is not present in the environment" — with the offending name preserved in detail. A concentration of MISSING_AXIOM under stats().reason_breakdown whose detail lines lead with unknown constant is the direct v0 signal to trigger a rename_map.json refresh, well before Layer 2's automated rewrite path is available.

Post-v0 Layer 2 (planned — spec §13): locate_first_error(kind = "unknown_constant") returns the position and the offending constant name from the first unknown constant diagnostic. When cross-referenced against a rename_map.json (maintained per toolchain bump), this supports semi-automatic rewriting of old names to their current equivalents. Layer 2 is a thin wrapper over v0 and does not introduce independent decision logic.

See also