Lean.Elab.Match

def Lean.Elab.Term.isAtomicDiscr? (discr : Lean.Syntax) :

We treat @x as atomic to avoid unnecessary extra local declarations from being inserted into the local context. Recall that expandMatchAltsIntoMatch uses @ modifier. Thus this is kind of discriminant is quite common.

Remark: if the discriminat is Systax.missing, we abort the elaboration of the match-expression. This can happen due to error recovery. Example

example : (p ∨ p) → p := fun h => match

If we don't abort, the elaborator loops because we will keep trying to expand

match

into

let d := ; match

Recall that Syntax.setArg stx i arg is a no-op when i is out-of-bounds.

Equations

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

source

structure Lean.Elab.Term.Discr:

Type

expr : Lean.Expr
some h if discriminant is annotated with the h : notation.
h? : Option Lean.Syntax

source

instance Lean.Elab.Term.instInhabitedDiscr:

Inhabited Lean.Elab.Term.Discr

Equations

Lean.Elab.Term.instInhabitedDiscr = { default := { expr := default, h? := default } }

source

structure Lean.Elab.Term.ElabMatchTypeAndDiscrsResult:

Type

discrs : Array Lean.Elab.Term.Discr
matchType : Lean.Expr
isDep : Bool
alts : Array Lean.Elab.Term.MatchAltView

source

def Lean.Elab.Term.expandMacrosInPatterns (matchAlts : Array Lean.Elab.Term.MatchAltView) :

Lean.MacroM (Array Lean.Elab.Term.MatchAltView)

Equations

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

source

def Lean.Elab.Term.elabInaccessible:

Lean.Elab.Term.TermElab

Equations

Lean.Elab.Term.elabInaccessible stx expectedType? = do let e ← Lean.Elab.Term.elabTerm (Lean.Syntax.getOp stx 1) expectedType? true true pure (Lean.mkInaccessible e)

source

def Lean.Elab.Term.precheckMatch:

Lean.Elab.Term.Quotation.Precheck

Equations

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

source

structure Lean.Elab.Term.PatternVarDecl:

Type

fvarId : Lean.FVarId

source

structure Lean.Elab.Term.PatternElabException:

Type

ex : Lean.Exception
patternIdx : Nat
pathToIndex : List Nat

source

structure Lean.Elab.Term.ToDepElimPattern.State:

Type

patternVars : Array Lean.Expr

source

structure Lean.Elab.Term.ToDepElimPattern.Context:

Type

When visiting an assigned metavariable, if it has an user-name. We save it here. We want to preserve these user-names when generating new pattern variables.
userName : Lean.Name
Pattern variables that were explicitly provided by the user. Recall that implicit parameters and _ are elaborated as metavariables, and then converted into pattern variables by the normalize procedure.
explicitPatternVars : Array Lean.FVarId

source

@[inline]

abbrev Lean.Elab.Term.ToDepElimPattern.M (α : Type) :

Type

Equations

Lean.Elab.Term.ToDepElimPattern.M = ReaderT Lean.Elab.Term.ToDepElimPattern.Context (StateRefT' IO.RealWorld Lean.Elab.Term.ToDepElimPattern.State Lean.Elab.TermElabM)

source

def Lean.Elab.Term.ToDepElimPattern.isExplicitPatternVar (e : Lean.Expr) :

Lean.Elab.Term.ToDepElimPattern.M Bool

Return true iff e is an explicit pattern variable provided by the user.

Equations

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

source

partial def Lean.Elab.Term.ToDepElimPattern.normalize (e : Lean.Expr) :

Lean.Elab.Term.ToDepElimPattern.M Lean.Expr

Normalize the pattern and collect all patterns variables (explicit and implicit). This method is the one that decides where the inaccessible annotations must be inserted. The pattern variables are both free variables (for explicit pattern variables) and metavariables (for implicit ones). Recall that mkLambdaFVars now allows us to abstract both free variables and metavariables.

source

def Lean.Elab.Term.ToDepElimPattern.normalize.addVar (e : Lean.Expr) :

Lean.Elab.Term.ToDepElimPattern.M Unit

Equations

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

source

def Lean.Elab.Term.ToDepElimPattern.normalize.processVar (e : Lean.Expr) :

Lean.Elab.Term.ToDepElimPattern.M Lean.Expr

Equations

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

source

partial def Lean.Elab.Term.ToDepElimPattern.normalize.processInaccessible (e : Lean.Expr) :

Lean.Elab.Term.ToDepElimPattern.M Lean.Expr

source

structure Lean.Elab.Term.ToDepElimPattern.TopSort.State:

Type

visitedFVars : Lean.FVarIdSet
visitedMVars : Lean.MVarIdSet
result : Array Lean.Expr

source

@[inline]

abbrev Lean.Elab.Term.ToDepElimPattern.TopSortM (α : Type) :

Type

Equations

Lean.Elab.Term.ToDepElimPattern.TopSortM = StateRefT' IO.RealWorld Lean.Elab.Term.ToDepElimPattern.TopSort.State Lean.Elab.TermElabM

source

def Lean.Elab.Term.ToDepElimPattern.savePatternInfo (p : Lean.Expr) :

Lean.Elab.TermElabM Lean.Expr

Save pattern information in the info tree, and remove patternWithRef? annotations.

Equations

Lean.Elab.Term.ToDepElimPattern.savePatternInfo p = ReaderT.run (Lean.Elab.Term.ToDepElimPattern.savePatternInfo.go p) false

source

partial def Lean.Elab.Term.ToDepElimPattern.savePatternInfo.go (p : Lean.Expr) :

ReaderT Bool Lean.Elab.TermElabM Lean.Expr

source

def Lean.Elab.Term.ToDepElimPattern.main {α : Type} (patternVarDecls : Array Lean.Elab.Term.PatternVarDecl) (ps : Array Lean.Expr) (matchType : Lean.Expr) (k : Array Lean.LocalDecl → Array Lean.Meta.Match.Pattern → Lean.Expr → Lean.Elab.TermElabM α) :

Lean.Elab.TermElabM α

Main method for withDepElimPatterns.

PatternVarDecls: are the explicit pattern variables provided by the user.
ps: are the patterns provided by the user.
matchType: the expected typ for this branch. It depends on the explicit pattern variables and the implicit ones that are still represented as metavariables, and are found by this function.
k is the continuation that is executed in an updated local context with the all pattern variables (explicit and implicit). Note that, patternVarDecls are all replaced since they may depend on implicit pattern variables (i.e., metavariables) that are converted into new free variables by this method.

Equations

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

source

def Lean.Elab.Term.ToDepElimPattern.main.pack (patternVars : Array Lean.Expr) (ps : Array Lean.Expr) (matchType : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

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

source

def Lean.Elab.Term.ToDepElimPattern.main.unpack {α : Type} (packed : Lean.Expr) (k : Array Lean.Expr → Array Lean.Expr → Lean.Expr → Lean.Elab.TermElabM α) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.ToDepElimPattern.main.unpack packed k = Lean.Elab.Term.ToDepElimPattern.main.unpack.go k packed #[]

source

partial def Lean.Elab.Term.ToDepElimPattern.main.unpack.go {α : Type} (k : Array Lean.Expr → Array Lean.Expr → Lean.Expr → Lean.Elab.TermElabM α) (packed : Lean.Expr) (patternVars : Array Lean.Expr) :

Lean.Elab.TermElabM α

source

def Lean.Elab.Term.withDepElimPatterns {α : Type} (patternVarDecls : Array Lean.Elab.Term.PatternVarDecl) (ps : Array Lean.Expr) (matchType : Lean.Expr) (k : Array Lean.LocalDecl → Array Lean.Meta.Match.Pattern → Lean.Expr → Lean.Elab.TermElabM α) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.withDepElimPatterns patternVarDecls ps matchType k = Lean.Elab.Term.ToDepElimPattern.main patternVarDecls ps matchType k

source

structure Lean.Elab.Term.GeneralizeResult:

Type

discrs : Array Lean.Elab.Term.Discr
FVarIds of the variables that have been generalized. We store them to clear after in each branch.
toClear : Array Lean.FVarId
matchType : Lean.Expr
altViews : Array Lean.Elab.Term.MatchAltView
refined : Bool

source

def Lean.Elab.Term.mkMatcher (input : Lean.Meta.Match.MkMatcherInput) :

Lean.Elab.TermElabM Lean.Meta.Match.MatcherResult

Equations

Lean.Elab.Term.mkMatcher input = liftM (Lean.Meta.Match.mkMatcher input)

source

opaque Lean.Elab.Term.match.ignoreUnusedAlts:

Lean.Option Bool

source

def Lean.Elab.Term.reportMatcherResultErrors (altLHSS : List Lean.Meta.Match.AltLHS) (result : Lean.Meta.Match.MatcherResult) :

Lean.Elab.TermElabM Unit

Equations

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

source

def Lean.Elab.Term.elabMatch:

Lean.Elab.Term.TermElab

Pattern matching. match e, ... with | p, ... => f | ... matches each given term e against each pattern p of a match alternative. When all patterns of an alternative match, the match term evaluates to the value of the corresponding right-hand side f with the pattern variables bound to the respective matched values.

Equations

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

source

def Lean.Elab.Term.elabMatch.elabMatchDefault (stx : Lean.Syntax) (expectedType? : Option Lean.Expr) :

Lean.Elab.TermElabM Lean.Expr

Equations

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

source

def Lean.Elab.Term.elabNoMatch:

Lean.Elab.Term.TermElab

Empty match/ex falso. nomatch e is of arbitrary type α : Sort u if Lean can show that an empty set of patterns is exhaustive given e's type, e.g. because it has no constructors.

Equations

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