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

Remark: if the discriminat 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.

Equations

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

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

Equations

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

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)

Equations

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

def Lean.Elab.Term.elabInaccessible : TermElab

Equations

• Lean.Elab.Term.elabInaccessible stx expectedType? = do let e ← Lean.Elab.Term.elabTerm stx[1] expectedType? pure (Lean.mkInaccessible e)

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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.

Equations

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

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

Equations

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

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

Equations

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

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 α

Equations

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

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

Equations

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

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

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

Equations

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

def Lean.Elab.Term.elabMatch : TermElab

Equations

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

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

Equations

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

def Lean.Elab.Term.elabNoMatch : TermElab

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Term.elabNoMatch.loop stx [] discrsNew = pure { raw := stx.setArg 1 (Lean.Syntax.mkSep discrsNew (Lean.mkAtomFrom stx ", ")) }

def Lean.Elab.Term.elabNoFun : TermElab

Equations

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