def Lean.Elab.Term.isAtomicDiscr (discr : Syntax) : TermElabM Bool

Remark: if the discriminant is Syntax.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 := <Syntax.missing>; match

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

structure Lean.Elab.Term.Discr : Type

• expr : Expr
• h? : Option Syntax

  some h if discriminant is annotated with the h : notation.

instance Lean.Elab.Term.instInhabitedDiscr : Inhabited Discr

structure Lean.Elab.Term.ElabMatchTypeAndDiscrsResult : Type

• discrs : Array Discr
• matchType : Expr
• isDep : Bool

  true when performing dependent elimination. We use this to decide whether we optimize the "match unit" case. See isMatchUnit?.

• alts : Array MatchAltView

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

def Lean.Elab.Term.getMatchAlt : Syntax → Option MatchAltView

Given the stx of a single match alternative, return a corresponding MatchAltView.

def Lean.Elab.Term.getMatchAlts : Syntax → Array MatchAltView

Given stx a match-expression, return its alternatives.

def Lean.Elab.Term.elabInaccessible : TermElab

def Lean.Elab.Term.precheckMatch : Quotation.Precheck

structure Lean.Elab.Term.PatternVarDecl : Type

We convert the collected PatternVars intro PatternVarDecl

• fvarId : FVarId

Remark: when performing dependent pattern matching, we often had to write code such as

def Vec.map' (f : α → β) (xs : Vec α n) : Vec β n :=
  match n, xs with
  | _, nil       => nil
  | _, cons a as => cons (f a) (map' f as)

We had to include n and the _s because the type of xs depends on n. Moreover, nil and cons a as have different types. This was quite tedious. So, we have implemented an automatic "discriminant refinement procedure". The procedure is based on the observation that we get a type error whenenver we forget to include _s and the indices a discriminant depends on. So, we catch the exception, check whether the type of the discriminant is an indexed family, and add their indices as new discriminants.

The current implementation, adds indices as they are found, and does not try to "sort" the new discriminants.

If the refinement process fails, we report the original error message.

structure Lean.Elab.Term.PatternElabException : Type

Auxiliary structure for storing an type mismatch exception when processing the pattern #idx of some alternative.

• ex : Exception
• patternIdx : Nat
• pathToIndex : List Nat

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

• patternVars : Array Expr

structure Lean.Elab.Term.ToDepElimPattern.Context : Type

• userName : Name

  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.

• explicitPatternVars : Array FVarId

  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.

@[reducible, inline]

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

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

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

partial def Lean.Elab.Term.ToDepElimPattern.normalize (e : Expr) : M 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.

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

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

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

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

• visitedFVars : FVarIdSet
• visitedMVars : MVarIdSet
• result : Array Expr

@[reducible, inline]

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

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

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

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

The Bool context is true iff we are inside of an "inaccessible" pattern.

def Lean.Elab.Term.ToDepElimPattern.main {α : Type} (patternVarDecls : Array PatternVarDecl) (ps : Array Expr) (matchType : Expr) (k : Array LocalDecl → Array Meta.Match.Pattern → Expr → TermElabM α) : 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.

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

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

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

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

structure Lean.Elab.Term.GeneralizeResult : Type

• discrs : Array Discr
• toClear : Array FVarId

  FVarIds of the variables that have been generalized. We store them to clear after in each branch.

• matchType : Expr
• altViews : Array MatchAltView
• refined : Bool

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

opaque Lean.Elab.Term.match.ignoreUnusedAlts : Lean.Option Bool

def Lean.Elab.Term.mkRedundantAlternativeMsg (altName? : Option Name) (altMsg? : Option MessageData) : MessageData

Constructs a "redundant alternative" error message.

Optionally accepts the name of the constructor (e.g., for use in the induction tactic) and/or the message-data representation of the alternative in question.

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

def Lean.Elab.Term.elabMatch : TermElab

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

def Lean.Elab.Term.elabNoMatch : TermElab

def Lean.Elab.Term.elabNoMatch.loop (stx : Syntax) (discrs : List Term) (discrsNew : Array Syntax) : TermElabM Term

def Lean.Elab.Term.elabNoFun : TermElab