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

`match_expr` alternative. Recall that it has the following structure.

    | (ident "@")? ident binderIdent* => 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 auxiliary continuation function for each right-hand-side.

- actuals : List Term

  Actual value to be passed as an argument.

Instances For

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

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

    | _ => rhs

- rhs : Syntax

Instances For

source
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] }

Instances For

source
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.

Instances For

source
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.

Instances For

source
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

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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 }

Instances For

source
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.

Instances For

source
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.

Instances For

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

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

Instances For

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

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

Instances For