Def Lean.Meta.RefinedDiscrTree.MatchResult.flatten

Modification history

2025-06-27 13:04

Mathlib/Lean/Meta/RefinedDiscrTree/Lookup.lean

feat: Interactive Library Rewrite (#11768) …

Added Lean.Meta.RefinedDiscrTree.MatchResult.flatten View on Github →