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 (k : SyntaxNodeKinds) : Type

• ref : Syntax
• patterns : Array Syntax
• lhs : Syntax
• rhs : TSyntax k

def Lean.Elab.Term.instInhabitedMatchAltView.default {a✝ : SyntaxNodeKinds} : MatchAltView a✝

Equations

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

@[implicit_reducible]

instance Lean.Elab.Term.instInhabitedMatchAltView {a✝ : SyntaxNodeKinds} : Inhabited (MatchAltView a✝)

Equations

• Lean.Elab.Term.instInhabitedMatchAltView = { default := Lean.Elab.Term.instInhabitedMatchAltView.default }