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.

Equations

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

def Lean.Elab.Term.MatchExpr.toAlt? (stx : Syntax) : Option 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 Alt) : List 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 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 = alts.any 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 Alt) (funName : Ident) : Option 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 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 _.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

def Lean.Elab.Term.MatchExpr.toDoubleQuotedName (ident : Ident) : 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 : 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.

Equations

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

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

Equations

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

def Lean.Elab.Term.expandMatchExpr : Macro

Equations

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

def Lean.Elab.Term.expandLetExpr : Macro

Equations

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