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

source
structure Lean.Elab.Term.MatchAltView :
Type

- ref : Syntax
- patterns : Array Syntax
- lhs : Syntax
- rhs : Syntax

Instances For

source
def Lean.Elab.Term.instInhabitedMatchAltView.default :
MatchAltView
Equations

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

Instances For

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

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