@[reducible, inline]

abbrev Lean.Elab.Term.PatternVar : Type

Patterns define new local variables. This module collect them and preprocess _ occurring in patterns. Recall that an _ may represent anonymous variables or inaccessible terms that are implied by typing constraints. Thus, we represent them with fresh named holes ?x. After we elaborate the pattern, if the metavariable remains unassigned, we transform it into a regular pattern variable. Otherwise, it becomes an inaccessible term.

Macros occurring in patterns are expanded before the collectPatternVars method is executed. The following kinds of Syntax are handled by this module

• Constructor applications
• Applications of functions tagged with the [match_pattern] attribute
• Identifiers
• Anonymous constructors
• Structure instances
• Inaccessible terms
• Named patterns
• Tuple literals
• Type ascriptions
• Literals: num, string and char

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

State for the pattern variable collector monad.

• found : Lean.NameSet

  Pattern variables found so far.

• vars : Array Lean.Elab.Term.PatternVar

  Pattern variables found so far as an array. It contains the order they were found.

instance Lean.Elab.Term.CollectPatternVars.instInhabitedState : Inhabited Lean.Elab.Term.CollectPatternVars.State

Equations

• Lean.Elab.Term.CollectPatternVars.instInhabitedState = { default := { found := default, vars := default } }

@[reducible, inline]

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

Equations

• Lean.Elab.Term.CollectPatternVars.M = StateRefT' IO.RealWorld Lean.Elab.Term.CollectPatternVars.State Lean.Elab.TermElabM

An application in a pattern can be

1- A constructor application The elaborator assumes fields are accessible and inductive parameters are not accessible.

2- A regular application (f ...) where f is tagged with [match_pattern]. The elaborator assumes implicit arguments are not accessible and explicit ones are accessible.

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

• funId : Lean.Ident
• ctorVal? : Option Lean.ConstructorVal
• explicit : Bool
• ellipsis : Bool
• paramDecls : Array (Lean.Name × Lean.BinderInfo)
• paramDeclIdx : Nat
• namedArgs : Array Lean.Elab.Term.NamedArg
• args : List Lean.Elab.Term.Arg
• newArgs : Array Lean.Term

instance Lean.Elab.Term.CollectPatternVars.instInhabitedContext : Inhabited Lean.Elab.Term.CollectPatternVars.Context

partial def Lean.Elab.Term.CollectPatternVars.collect (stx : Lean.Syntax) : Lean.Elab.Term.CollectPatternVars.M Lean.Syntax

partial def Lean.Elab.Term.CollectPatternVars.collect.processCtorApp (stx : Lean.Syntax) : Lean.Elab.Term.CollectPatternVars.M Lean.Syntax

partial def Lean.Elab.Term.CollectPatternVars.collect.processCtor (stx : Lean.Syntax) : Lean.Elab.Term.CollectPatternVars.M Lean.Syntax

partial def Lean.Elab.Term.CollectPatternVars.collect.processId (stx : Lean.Syntax) : Lean.Elab.Term.CollectPatternVars.M Lean.Syntax

Check whether stx is a pattern variable or constructor-like (i.e., constructor or constant tagged with [match_pattern] attribute)

partial def Lean.Elab.Term.CollectPatternVars.collect.pushNewArg (accessible : Bool) (ctx : Lean.Elab.Term.CollectPatternVars.Context) (arg : Lean.Elab.Term.Arg) : Lean.Elab.Term.CollectPatternVars.M Lean.Elab.Term.CollectPatternVars.Context

partial def Lean.Elab.Term.CollectPatternVars.collect.processExplicitArg (accessible : Bool) (ctx : Lean.Elab.Term.CollectPatternVars.Context) : Lean.Elab.Term.CollectPatternVars.M Lean.Elab.Term.CollectPatternVars.Context

partial def Lean.Elab.Term.CollectPatternVars.collect.processImplicitArg (accessible : Bool) (ctx : Lean.Elab.Term.CollectPatternVars.Context) : Lean.Elab.Term.CollectPatternVars.M Lean.Elab.Term.CollectPatternVars.Context

partial def Lean.Elab.Term.CollectPatternVars.collect.processCtorAppContext (ctx : Lean.Elab.Term.CollectPatternVars.Context) : Lean.Elab.Term.CollectPatternVars.M Lean.Syntax

partial def Lean.Elab.Term.CollectPatternVars.collect.processCtorAppCore (f : Lean.Syntax) (namedArgs : Array Lean.Elab.Term.NamedArg) (args : Array Lean.Elab.Term.Arg) (ellipsis : Bool) : Lean.Elab.Term.CollectPatternVars.M Lean.Syntax

def Lean.Elab.Term.CollectPatternVars.main (alt : Lean.Elab.Term.MatchAltView) : Lean.Elab.Term.CollectPatternVars.M Lean.Elab.Term.MatchAltView

def Lean.Elab.Term.collectPatternVars (alt : Lean.Elab.Term.MatchAltView) : Lean.Elab.TermElabM (Array Lean.Elab.Term.PatternVar × Lean.Elab.Term.MatchAltView)

Collect pattern variables occurring in the match-alternative object views. It also returns the updated views.

def Lean.Elab.Term.getPatternVars (patternStx : Lean.Syntax) : Lean.Elab.TermElabM (Array Lean.Elab.Term.PatternVar)

Return the pattern variables in the given pattern. Remark: this method is not used by the main match elaborator, but in the precheck hook and other macros (e.g., at Do.lean).

def Lean.Elab.Term.getPatternsVars (patterns : Array Lean.Syntax) : Lean.Elab.TermElabM (Array Lean.Elab.Term.PatternVar)

Return the pattern variables occurring in the given patterns. This method is used in the match and do notation elaborators

Equations

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

def Lean.Elab.Term.getPatternVarNames (pvars : Array Lean.Elab.Term.PatternVar) : Array Lean.Name

Equations

• Lean.Elab.Term.getPatternVarNames pvars = Array.map (fun (x : Lean.Elab.Term.PatternVar) => Lean.Syntax.getId x) pvars