structure Lean.Elab.Term.MatchExpr.Alt : Type

match_expr alternative. Recall that it has the following structure.

| (ident "@")? ident bindeIdent* => rhs

Example:

| c@Eq _ a b => f c a b

• var? : Option Ident

  some c if there is a variable binding to the function symbol being matched. c is the variable name.

• funName : Ident

  Function being matched.

• pvars : List (Option Ident)

  Pattern variables. The list uses none for representing _, and some a for pattern variable a.

• rhs : Syntax

  right-hand-side for the alternative.

• k : Ident

  Store the auxliary continuation function for each right-hand-side.

• actuals : List Term

  Actual value to be passed as an argument.

structure Lean.Elab.Term.MatchExpr.ElseAlt : Type

match_expr else-alternative. Recall that it has the following structure.

| _ => rhs

• rhs : Syntax

def Lean.Elab.Term.MatchExpr.toElseAlt? (stx : Syntax) : Option ElseAlt

Converts syntax representing a match_expr else-alternative into an ElseAlt.

def Lean.Elab.Term.MatchExpr.toAlt? (stx : Syntax) : Option Alt

Converts syntax representing a match_expr alternative into an Alt.

def Lean.Elab.Term.MatchExpr.getFunNamesToMatch (alts : List Alt) : List Ident

Returns the function names of alternatives that do not have any pattern variable left.

def Lean.Elab.Term.MatchExpr.shouldSaveActual (alts : List Alt) : Bool

Returns true if there is at least one alternative whose next pattern variable is not a _.

def Lean.Elab.Term.MatchExpr.getAltFor? (alts : List Alt) (funName : Ident) : Option Alt

Returns the first alternative whose function name is funName and does not have pattern variables left to match.

def Lean.Elab.Term.MatchExpr.next (alts : List Alt) (actual : Term) : List Alt

Removes alternatives that do not have any pattern variable left to be matched. For the ones that still have pattern variables, remove the first one, and save actual if the removed pattern variable is not a _.

def Lean.Elab.Term.MatchExpr.initK (alt : Alt) : MacroM Alt

Creates a fresh identifier for representing the continuation function used to execute the RHS of the given alternative, and stores it in the field k.

def Lean.Elab.Term.MatchExpr.getParams (alt : Alt) : MacroM (Array (TSyntax `Lean.Parser.Term.bracketedBinder))

Generates parameters for the continuation function used to execute the RHS of the given alternative.

def Lean.Elab.Term.MatchExpr.getActuals (discr : Term) (alt : Alt) : MacroM (Array Term)

Generates the actual arguments for invoking the auxiliary continuation function associated with the given alternative. The arguments are the actuals stored in alt. discr is also an argument if alt.var? is not none.

def Lean.Elab.Term.MatchExpr.toDoubleQuotedName (ident : Ident) : Term

def Lean.Elab.Term.MatchExpr.generate (discr : Term) (alts : List Alt) (elseAlt : ElseAlt) : MacroM Syntax

Generates an if-then-else tree for implementing a match_expr with discriminant discr, alternatives alts, and else-alternative elseAlt.

partial def Lean.Elab.Term.MatchExpr.generate.loop (kElse : TSyntax `term) (discr : Term) (alts : List Alt) : MacroM Term

def Lean.Elab.Term.MatchExpr.main (discr : Term) (alts : Array Syntax) (elseAlt : Syntax) : MacroM Syntax

def Lean.Elab.Term.expandMatchExpr : Macro

def Lean.Elab.Term.expandLetExpr : Macro