def Lean.Elab.Term.isAtomicDiscr (discr : Lean.Syntax) : Lean.Elab.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 : Lean.Expr
• h? : Option Lean.Syntax

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

instance Lean.Elab.Term.instInhabitedDiscr : Inhabited Lean.Elab.Term.Discr

structure Lean.Elab.Term.ElabMatchTypeAndDiscrsResult : Type

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

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

• alts : Array Lean.Elab.Term.MatchAltView

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

def Lean.Elab.Term.elabInaccessible : Lean.Elab.Term.TermElab

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

structure Lean.Elab.Term.PatternVarDecl : Type

We convert the collected PatternVars intro PatternVarDecl

• fvarId : Lean.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 : Lean.Exception
• patternIdx : Nat
• pathToIndex : List Nat

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

• patternVars : Array Lean.Expr

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

• userName : Lean.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 Lean.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 : Lean.Expr) : Lean.Elab.Term.ToDepElimPattern.M Bool

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

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.

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

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.

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

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

• visitedFVars : Lean.FVarIdSet
• visitedMVars : Lean.MVarIdSet
• result : Array Lean.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 : 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 = (Lean.Elab.Term.ToDepElimPattern.savePatternInfo.go p).run false

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

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

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.

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

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 α

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 α

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 α

structure Lean.Elab.Term.GeneralizeResult : Type

• discrs : Array Lean.Elab.Term.Discr
• toClear : Array Lean.FVarId

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

• matchType : Lean.Expr
• altViews : Array Lean.Elab.Term.MatchAltView
• refined : Bool

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)

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

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

def Lean.Elab.Term.elabMatch : Lean.Elab.Term.TermElab

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

def Lean.Elab.Term.elabNoMatch : Lean.Elab.Term.TermElab

Equations

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

def Lean.Elab.Term.elabNoMatch.loop (stx : Lean.Syntax) (discrs : List Lean.Term) (discrsNew : Array Lean.Syntax) : Lean.Elab.TermElabM Lean.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 : Lean.Elab.Term.TermElab

Equations

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