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 Lean.Ident

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

• funName : Lean.Ident

  Function being matched.

• pvars : List (Option Lean.Ident)

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

• rhs : Lean.Syntax

  right-hand-side for the alternative.

• k : Lean.Ident

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

• actuals : List Lean.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 : Lean.Syntax

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

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

Equations

• Lean.Elab.Term.MatchExpr.toElseAlt? stx = if (!Lean.Syntax.isOfKind stx `Lean.Parser.Term.matchExprElseAlt) = true then none else some { rhs := stx[3] }

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

Converts syntax representing a match_expr alternative into an Alt.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Lean.Elab.Term.MatchExpr.shouldSaveActual alts = List.any alts fun (alt : Lean.Elab.Term.MatchExpr.Alt) => match alt.pvars with | some val :: tail => true | x => false

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

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.MatchExpr.next (alts : List Lean.Elab.Term.MatchExpr.Alt) (actual : Lean.Term) : List Lean.Elab.Term.MatchExpr.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 _.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.MatchExpr.initK (alt : Lean.Elab.Term.MatchExpr.Alt) : Lean.MacroM Lean.Elab.Term.MatchExpr.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.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.MatchExpr.getActuals (discr : Lean.Term) (alt : Lean.Elab.Term.MatchExpr.Alt) : Lean.MacroM (Array Lean.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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.Term.MatchExpr.toDoubleQuotedName ident = { raw := (Lean.mkNode `Lean.Parser.Term.doubleQuotedName #[Lean.mkAtom "`", Lean.mkAtom "`", ident.raw]).raw }

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.expandMatchExpr : Lean.Macro

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.expandLetExpr : Lean.Macro

Equations

• One or more equations did not get rendered due to their size.