feat: add structured TraceResult to TraceData#12698

Merged

kim-em merged 9 commits intoleanprover:masterfrom

kim-em:kim/trace-result-field

Mar 10, 2026

Commits on Mar 10, 2026

feat: add structured `TraceResult` to `TraceData`

kim-em
and
claude
committed
fix: don't infer TraceResult from Except.isOk in withTraceNode

kim-em
and
claude
committed
refactor: change result? to mkResult? callback on withTraceNode/withTraceNodeBefore

kim-em
and
claude
committed
feat: add TraceResult.error for bombEmoji (exceptions)

kim-em
and
claude
committed
refactor: replace ExceptToEmoji with ExceptToTraceResult

kim-em
and
claude
committed
refactor: address review feedback on TraceResult API

kim-em
and
claude
committed
refactor: remove manual emoji from withTraceNode callers

kim-em
and
claude
committed
refactor: revert unrelated SubExpr.lean style change

kim-em
and
claude
committed
test: update expected output after rebase

kim-em
and
claude
committed