@[reducible, inline]

abbrev Lean.Elab.Term.PatternVar : Type

Patterns define new local variables. This module collects them and preprocesses _ 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 : NameSet

  Pattern variables found so far.

• vars : Array PatternVar

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

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

@[reducible, inline]

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

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 : Ident
• ctorVal? : Option ConstructorVal
• explicit : Bool
• ellipsis : Bool
• paramDecls : Array (Name × BinderInfo)
• paramDeclIdx : Nat
• namedArgs : Array NamedArg
• args : List Arg
• newArgs : Array Term

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

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

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

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

partial def Lean.Elab.Term.CollectPatternVars.collect.processId (stx : Syntax) : M 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 : Context) (arg : Arg) : M Context

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

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

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

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

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

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

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

def Lean.Elab.Term.getPatternVars (patternStx : Syntax) : TermElabM (Array 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 Syntax) : TermElabM (Array PatternVar)

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

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