feat: add TraceData.headerContent? for pre-emoji header access `withTraceNodeBefore` prepends `TraceResult.toEmoji` to the header before storing it in the trace tree. This makes it difficult for programmatic consumers to compare headers across trace runs, since the same check gets different emoji prefixes depending on success/failure. Add `headerContent? : Option MessageData` to `TraceData` that stores the original pre-emoji header content. This is purely additive — the emoji-prefixed header continues to be stored as before, and all existing trace output is unchanged. Closes #13069 Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.