Documentation

Lean.Elab.PatternVar

@[inline]

abbrev Lean.Elab.Term.PatternVar:

Type

Equations

Lean.Elab.Term.PatternVar = Lean.Syntax

structure Lean.Elab.Term.CollectPatternVars.State:

Type

found : Lean.NameSet
vars : Array Lean.Elab.Term.PatternVar

instance Lean.Elab.Term.CollectPatternVars.instInhabitedState:

Inhabited Lean.Elab.Term.CollectPatternVars.State

Equations

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

@[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

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

Equations

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

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

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

Equations

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

def Lean.Elab.Term.collectPatternVars (alt : Lean.Elab.Term.MatchAltView) :

Lean.Elab.TermElabM (Array Lean.Elab.Term.PatternVar × Lean.Elab.Term.MatchAltView)

Equations

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

def Lean.Elab.Term.getPatternVars (patternStx : Lean.Syntax) :

Lean.Elab.TermElabM (Array Lean.Elab.Term.PatternVar)

Equations

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

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

Lean.Elab.TermElabM (Array Lean.Elab.Term.PatternVar)

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.Syntax.getId x) pvars