commit: c40d38f28443cf379c6e20b7af6c0510eaca35d9

[log]
author: Sebastian Ullrich <sebasti@nullri.ch>

Sun Sep 20 11:05:00 2026 +0000
committer: Sebastian Ullrich <sebasti@nullri.ch>

Sun Sep 20 15:58:51 2026 +0000
tree: a0de4ba8f41c3cb5de814790a147771e3ad04774
parent: abdbf8d7833b734207c7b75bbc32098384a4d78c [diff]

fix: name the realized constant in the missing `enableRealizationsForConst` error

This PR makes `realizeConst` report the constant being realized when `enableRealizationsForConst` has not been called for its target, instead of the mangled private name of the internal key type that the generic `realizeValue` check can only show.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

2 files changed

tree: a0de4ba8f41c3cb5de814790a147771e3ad04774

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.