Inductive Lean.MessageData.TraceResult

Modification history

2026-04-04 23:52
Mathlib/Lean/MessageData/Trace.lean
chore: bump toolchain to v4.30.0-rc1 (#37564)
Deleted Lean.MessageData.TraceResultView on Github →
2026-03-01 06:36
Mathlib/Lean/MessageData/Trace.lean
feat(Tactic): add `#defeq_abuse` tactic combinator (#35750) …
Added Lean.MessageData.TraceResultView on Github →