structure Lean.Meta.Grind.SymbolPriorities : Type

grind uses symbol priorities when inferring patterns for E-matching. Symbols not in map are assumed to have default priority (i.e., eval_prio default).

• map : PHashMap Name Nat

instance Lean.Meta.Grind.instInhabitedSymbolPriorities : Inhabited SymbolPriorities

structure Lean.Meta.Grind.SymbolPriorityEntry : Type

• declName : Name
• prio : Nat

instance Lean.Meta.Grind.instInhabitedSymbolPriorityEntry : Inhabited SymbolPriorityEntry

def Lean.Meta.Grind.SymbolPriorities.erase (s : SymbolPriorities) (declName : Name) : SymbolPriorities

Removes the given declaration from s.

def Lean.Meta.Grind.SymbolPriorities.insert (s : SymbolPriorities) (declName : Name) (prio : Nat) : SymbolPriorities

Inserts declName ↦ prio into s.

def Lean.Meta.Grind.SymbolPriorities.getPrio (s : SymbolPriorities) (declName : Name) : Nat

Returns declName priority for E-matching pattern inference in s.

def Lean.Meta.Grind.SymbolPriorities.contains (s : SymbolPriorities) (declName : Name) : Bool

Returns true, if there is an entry declName ↦ prio in s. Recall that symbols not in s are assumed to have default priority.

def Lean.Meta.Grind.resetSymbolPrioExt : CoreM Unit

def Lean.Meta.Grind.getGlobalSymbolPriorities : CoreM SymbolPriorities

def Lean.Meta.Grind.addSymbolPriorityAttr (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit

Sets declName priority to be used during E-matching pattern inference

def Lean.Meta.Grind.mkOffsetPattern (pat : Expr) (k : Nat) : Expr

def Lean.Meta.Grind.isOffsetPattern? (pat : Expr) : Option (Expr × Nat)

def Lean.Meta.Grind.mkEqBwdPattern (u : List Level) (α lhs rhs : Expr) : Expr

def Lean.Meta.Grind.isEqBwdPattern (e : Expr) : Bool

def Lean.Meta.Grind.isEqBwdPattern? (e : Expr) : Option (Expr × Expr)

def Lean.Meta.Grind.mkGenPattern (u : List Level) (α h x val : Expr) : Expr

def Lean.Meta.Grind.mkGenHEqPattern (u : List Level) (α β h x val : Expr) : Expr

structure Lean.Meta.Grind.GenPatternInfo : Type

Generalized pattern information. See Grind.genPattern gadget.

• heq : Bool
• hIdx : Nat
• xIdx : Nat

instance Lean.Meta.Grind.instReprGenPatternInfo : Repr GenPatternInfo

def Lean.Meta.Grind.isGenPattern? (pat : Expr) : Option (GenPatternInfo × Expr)

def Lean.Meta.Grind.isMatchCongrEqDeclName (declName : Name) : CoreM Bool

Returns true if declName is the name of a match-expression congruence equation.

theorem Lean.Meta.Grind.normConfig_zeta : Lean.Meta.Grind.normConfig✝.zeta = true

theorem Lean.Meta.Grind.normConfig_zetaDelta : Lean.Meta.Grind.normConfig✝.zetaDelta = true

def Lean.Meta.Grind.preprocessPattern (pat : Expr) (normalizePattern : Bool := true) : MetaM Expr

inductive Lean.Meta.Grind.Origin : Type

• decl (declName : Name) : Origin

  A global declaration in the environment.

• fvar (fvarId : FVarId) : Origin

  A local hypothesis.

• stx (id : Name) (ref : Syntax) : Origin

  A proof term provided directly to a call to grind where ref is the provided grind argument. The id is a unique identifier for the call.

• local (id : Name) : Origin

  It is local, but we don't have a local hypothesis for it.

instance Lean.Meta.Grind.instInhabitedOrigin : Inhabited Origin

instance Lean.Meta.Grind.instReprOrigin : Repr Origin

def Lean.Meta.Grind.Origin.key : Origin → Name

A unique identifier corresponding to the origin.

def Lean.Meta.Grind.Origin.pp {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (o : Origin) : m MessageData

instance Lean.Meta.Grind.instBEqOrigin : BEq Origin

instance Lean.Meta.Grind.instHashableOrigin : Hashable Origin

inductive Lean.Meta.Grind.EMatchTheoremKind : Type

• eqLhs (gen : Bool) : EMatchTheoremKind
• eqRhs (gen : Bool) : EMatchTheoremKind
• eqBoth (gen : Bool) : EMatchTheoremKind
• eqBwd : EMatchTheoremKind
• fwd : EMatchTheoremKind
• bwd (gen : Bool) : EMatchTheoremKind
• leftRight : EMatchTheoremKind
• rightLeft : EMatchTheoremKind
• default (gen : Bool) : EMatchTheoremKind
• user : EMatchTheoremKind

instance Lean.Meta.Grind.instInhabitedEMatchTheoremKind : Inhabited EMatchTheoremKind

instance Lean.Meta.Grind.instBEqEMatchTheoremKind : BEq EMatchTheoremKind

instance Lean.Meta.Grind.instReprEMatchTheoremKind : Repr EMatchTheoremKind

instance Lean.Meta.Grind.instHashableEMatchTheoremKind : Hashable EMatchTheoremKind

def Lean.Meta.Grind.EMatchTheoremKind.isEqLhs : EMatchTheoremKind → Bool

def Lean.Meta.Grind.EMatchTheoremKind.isDefault : EMatchTheoremKind → Bool

structure Lean.Meta.Grind.EMatchTheorem : Type

A theorem for heuristic instantiation based on E-matching.

• levelParams : Array Name

  It stores universe parameter names for universe polymorphic proofs. Recall that it is non-empty only when we elaborate an expression provided by the user. When proof is just a constant, we can use the universe parameter names stored in the declaration.

• proof : Expr
• numParams : Nat
• patterns : List Expr
• symbols : List HeadIndex

  Contains all symbols used in patterns.

• origin : Origin
• kind : EMatchTheoremKind

  The kind is used for generating the patterns. We save it here to implement grind?.

instance Lean.Meta.Grind.instInhabitedEMatchTheorem : Inhabited EMatchTheorem

structure Lean.Meta.Grind.EMatchTheorems : Type

Set of E-matching theorems.

• smap : Lean.PHashMap Lean.Name (List Lean.Meta.Grind.EMatchTheorem)

  The key is a symbol from EMatchTheorem.symbols.

• origins : Lean.PHashSet Lean.Meta.Grind.Origin

  Set of theorem ids that have been inserted using insert.

• erased : Lean.PHashSet Lean.Meta.Grind.Origin

  Theorems that have been marked as erased

• omap : Lean.PHashMap Lean.Meta.Grind.Origin (List Lean.Meta.Grind.EMatchTheorem)

  Mapping from origin to E-matching theorems associated with this origin.

• prios : Lean.Meta.Grind.SymbolPriorities

  Priorities for pattern inference

instance Lean.Meta.Grind.instInhabitedEMatchTheorems : Inhabited EMatchTheorems

def Lean.Meta.Grind.EMatchTheorems.insert (s : EMatchTheorems) (thm : EMatchTheorem) : EMatchTheorems

Inserts a thm with symbols [s_1, ..., s_n] to s. We add s_1 -> { thm with symbols := [s_2, ..., s_n] }. When grind internalizes a term containing symbol s, we process all theorems thm associated with key s. If their thm.symbols is empty, we say they are activated. Otherwise, we reinsert into map.

def Lean.Meta.Grind.EMatchTheorems.contains (s : EMatchTheorems) (origin : Origin) : Bool

Returns true if s contains a theorem with the given origin.

def Lean.Meta.Grind.EMatchTheorems.erase (s : EMatchTheorems) (origin : Origin) : EMatchTheorems

Mark the theorem with the given origin as erased

def Lean.Meta.Grind.EMatchTheorems.isErased (s : EMatchTheorems) (origin : Origin) : Bool

Returns true if the theorem has been marked as erased.

@[inline]

def Lean.Meta.Grind.EMatchTheorems.retrieve? (s : EMatchTheorems) (sym : Name) : Option (List EMatchTheorem × EMatchTheorems)

Retrieves theorems from s associated with the given symbol. See EMatchTheorem.insert. The theorems are removed from s.

def Lean.Meta.Grind.EMatchTheorems.find (s : EMatchTheorems) (origin : Origin) : List EMatchTheorem

Returns theorems associated with the given origin.

def Lean.Meta.Grind.EMatchTheorem.getProofWithFreshMVarLevels (thm : EMatchTheorem) : MetaM Expr

def Lean.Meta.Grind.isEMatchTheorem (declName : Name) : CoreM Bool

Returns true if declName has been tagged as an E-match theorem using [grind].

def Lean.Meta.Grind.resetEMatchTheoremsExt : CoreM Unit

partial def Lean.Meta.Grind.splitWhileForbidden (pat : Expr) : List Expr

Auxiliary function to expand a pattern containing forbidden application symbols into a multi-pattern.

This function enhances the usability of the [grind =] attribute by automatically handling forbidden pattern symbols. For example, consider the following theorem tagged with this attribute:

getLast?_eq_some_iff {xs : List α} {a : α} : xs.getLast? = some a ↔ ∃ ys, xs = ys ++ [a]

Here, the selected pattern is xs.getLast? = some a, but Eq is a forbidden pattern symbol. Instead of producing an error, this function converts the pattern into a multi-pattern, allowing the attribute to be used conveniently.

The function recursively expands patterns with forbidden symbols by splitting them into their sub-components. If the pattern does not contain forbidden symbols, it is returned as-is.

def Lean.Meta.Grind.mkGroundPattern (e : Expr) : Expr

def Lean.Meta.Grind.groundPattern? (e : Expr) : Option Expr

def Lean.Meta.Grind.isPatternDontCare (e : Expr) : Bool

partial def Lean.Meta.Grind.ppPattern (pattern : Expr) : MessageData

partial def Lean.Meta.Grind.ppPattern.ppArg (arg : Expr) : MessageData

structure Lean.Meta.Grind.NormalizePattern.State : Type

• symbols : Array HeadIndex
• symbolSet : Std.HashSet HeadIndex
• bvarsFound : Std.HashSet Nat

@[reducible, inline]

abbrev Lean.Meta.Grind.NormalizePattern.M (α : Type) : Type

def Lean.Meta.Grind.NormalizePattern.isCandidateSymbol (declName : Name) (root : Bool) : M Bool

inductive Lean.Meta.Grind.NormalizePattern.PatternArgKind : Type

• relevant : PatternArgKind

  Argument is relevant for E-matching.

• instImplicit : PatternArgKind

  Instance implicit arguments are considered support and handled using isDefEq.

• proof : PatternArgKind

  Proofs are ignored during E-matching. Lean is proof irrelevant.

• typeFormer : PatternArgKind

  Types and type formers are mostly ignored during E-matching, and processed using isDefEq. However, if the argument is of the form C .. where C is inductive type we process it as part of the pattern. Suppose we have as bs : List α, and a pattern candidate expression as ++ bs, i.e., @HAppend.hAppend (List α) (List α) (List α) inst as bs. If we completely ignore the types, the pattern will just be

  @HAppend.hAppend _ _ _ _ #1 #0
  

  This is not ideal because the E-matcher will try it in any goal that contains ++, even if it does not even mention lists.

instance Lean.Meta.Grind.NormalizePattern.instReprPatternArgKind : Repr PatternArgKind

def Lean.Meta.Grind.NormalizePattern.PatternArgKind.isSupport : PatternArgKind → Bool

def Lean.Meta.Grind.NormalizePattern.getPatternArgKinds (f : Expr) (numArgs : Nat) : MetaM (Array PatternArgKind)

Returns an array kinds s.ts kinds[i] is the kind of the corresponding argument.

• a type (that is not a proposition) or type former (which has forward dependencies) or
• a proof, or
• an instance implicit argument

When kinds[i].isSupport is true, we say the corresponding argument is a "support" argument.

def Lean.Meta.Grind.NormalizePattern.main (patterns : List Expr) (symPrios : SymbolPriorities) (minPrio : Nat) : MetaM (List Expr × List HeadIndex × Std.HashSet Nat)

def Lean.Meta.Grind.NormalizePattern.normalizePattern (e : Expr) : M Expr

inductive Lean.Meta.Grind.CheckCoverageResult : Type

Auxiliary type for the checkCoverage function.

• ok : CheckCoverageResult

  checkCoverage succeeded

• missing (pos : List Nat) : CheckCoverageResult

  checkCoverage failed because some of the theorem parameters are missing, pos contains their positions

def Lean.Meta.Grind.mkEMatchTheoremCore (origin : Origin) (levelParams : Array Name) (numParams : Nat) (proof : Expr) (patterns : List Expr) (kind : EMatchTheoremKind) (showInfo : Bool := false) : MetaM EMatchTheorem

Creates an E-matching theorem for a theorem with proof proof, numParams parameters, and the given set of patterns. Pattern variables are represented using de Bruijn indices.

def Lean.Meta.Grind.mkEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) (kind : EMatchTheoremKind) : MetaM EMatchTheorem

Creates an E-matching theorem for declName with numParams parameters, and the given set of patterns. Pattern variables are represented using de Bruijn indices.

def Lean.Meta.Grind.mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) (normalizePattern useLhs gen : Bool) (showInfo : Bool := false) : MetaM EMatchTheorem

Given a theorem with proof proof and type of the form ∀ (a_1 ... a_n), lhs = rhs, creates an E-matching pattern for it using addEMatchTheorem n [lhs] If normalizePattern is true, it applies the grind simplification theorems and simprocs to the pattern.

def Lean.Meta.Grind.mkEMatchEqBwdTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) (showInfo : Bool := false) : MetaM EMatchTheorem

def Lean.Meta.Grind.mkEMatchEqTheorem (declName : Name) (normalizePattern useLhs : Bool := true) (gen showInfo : Bool := false) : MetaM EMatchTheorem

Given theorem with name declName and type of the form ∀ (a_1 ... a_n), lhs = rhs, creates an E-matching pattern for it using addEMatchTheorem n [lhs]

If normalizePattern is true, it applies the grind simplification theorems and simprocs to the pattern.

def Lean.Meta.Grind.addEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) (kind : EMatchTheoremKind) : MetaM Unit

Adds an E-matching theorem to the environment. See mkEMatchTheorem.

def Lean.Meta.Grind.addEMatchEqTheorem (declName : Name) : MetaM Unit

Adds an E-matching equality theorem to the environment. See mkEMatchEqTheorem.

def Lean.Meta.Grind.getEMatchTheorems : CoreM EMatchTheorems

Returns the E-matching theorems registered in the environment.

def Lean.Meta.Grind.EMatchTheoremKind.gen : EMatchTheoremKind → Bool

def Lean.Meta.Grind.mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : EMatchTheoremKind) (symPrios : SymbolPriorities) (groundPatterns : Bool := true) (showInfo : Bool := false) : MetaM (Option EMatchTheorem)

Creates an E-match theorem using the given proof and kind. If groundPatterns is true, it accepts patterns without pattern variables. This is useful for theorems such as theorem evenZ : Even 0. For local theorems, we use groundPatterns := false since the theorem is already in the grind state and there is nothing to be instantiated.

def Lean.Meta.Grind.mkEMatchTheoremWithKind?.collect (proof : Expr) (symPrios : SymbolPriorities) (groundPatterns : Bool := true) (xs searchPlaces : Array Expr) : MetaM (Option (List Expr × List HeadIndex))

def Lean.Meta.Grind.mkEMatchTheoremWithKind?.go (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : EMatchTheoremKind) (symPrios : SymbolPriorities) (groundPatterns : Bool := true) (showInfo : Bool := false) (xs searchPlaces : Array Expr) : MetaM (Option EMatchTheorem)

def Lean.Meta.Grind.mkEMatchTheoremForDecl (declName : Name) (thmKind : EMatchTheoremKind) (prios : SymbolPriorities) (showInfo : Bool := false) : MetaM EMatchTheorem

def Lean.Meta.Grind.mkEMatchEqTheoremsForDef? (declName : Name) (showInfo : Bool := false) : MetaM (Option (Array EMatchTheorem))

def Lean.Meta.Grind.EMatchTheorems.eraseDecl (s : EMatchTheorems) (declName : Name) : MetaM EMatchTheorems

def Lean.Meta.Grind.addEMatchAttr (declName : Name) (attrKind : AttributeKind) (thmKind : EMatchTheoremKind) (prios : SymbolPriorities) (showInfo : Bool := false) : MetaM Unit

def Lean.Meta.Grind.eraseEMatchAttr (declName : Name) : MetaM Unit