Def Lean.MessageData.stripTraceResultPrefix

Modification history

2026-03-01 06:36
Mathlib/Lean/MessageData/Trace.lean
feat(Tactic): add `#defeq_abuse` tactic combinator (#35750) …
Added Lean.MessageData.stripTraceResultPrefixView on Github →