This module assumes match-expressions use the following syntax.

def matchDiscr := leading_parser optional (try (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> termParser

def «match» := leading_parser:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts

structure Lean.Elab.Term.MatchAltView : Type

• ref : Lean.Syntax
• patterns : Array Lean.Syntax
• rhs : Lean.Syntax

instance Lean.Elab.Term.instInhabitedMatchAltView : Inhabited Lean.Elab.Term.MatchAltView

Equations

• Lean.Elab.Term.instInhabitedMatchAltView = { default := { ref := default, patterns := default, rhs := default } }