Design Note: Symbol Priorities and Extension State

We considered including SymbolPriorities in ExtensionState to allow each grind attribute/extension to define its own symbol priorities. However, this design was rejected because E-match patterns are selected with respect to symbol priorities. When using multiple grind attributes simultaneously (e.g., grind only [attr_1, attr_2]), patterns would need to be re-selected using the union of all symbol priorities and then re-normalized using the union of all normalizers, an expensive operation we want to avoid.

Instead, we use a single global SymbolPriorities set shared across all grind attributes. See also: the related note in Extension.lean regarding normalization.

structure Lean.Meta.Grind.SymbolPriorityEntry : Type

• declName : Name
• prio : Nat

def Lean.Meta.Grind.instInhabitedSymbolPriorityEntry.default : SymbolPriorityEntry

Equations

• Lean.Meta.Grind.instInhabitedSymbolPriorityEntry.default = { declName := default, prio := default }

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedSymbolPriorityEntry : Inhabited SymbolPriorityEntry

Equations

• Lean.Meta.Grind.instInhabitedSymbolPriorityEntry = { default := Lean.Meta.Grind.instInhabitedSymbolPriorityEntry.default }

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

Removes the given declaration from s.

Equations

• s.erase declName = { map := Lean.PersistentHashMap.erase s.map declName }

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

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

Equations

• s.getPrio declName = match Lean.PersistentHashMap.find? s.map declName with | some prio => prio | x => 1000

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.

Equations

• s.contains declName = Lean.PersistentHashMap.contains s.map declName

def Lean.Meta.Grind.resetSymbolPrioExt : CoreM Unit

Equations

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

def Lean.Meta.Grind.getGlobalSymbolPriorities : CoreM SymbolPriorities

Equations

• Lean.Meta.Grind.getGlobalSymbolPriorities = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.Grind.symbolPrioExt✝ __do_lift)

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

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

Equations

• Lean.Meta.Grind.addSymbolPriorityAttr declName attrKind prio = Lean.ScopedEnvExtension.add Lean.Meta.Grind.symbolPrioExt✝ { declName := declName, prio := prio } attrKind

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

Equations

• Lean.Meta.Grind.mkOffsetPattern pat k = Lean.mkApp2 (Lean.mkConst `Lean.Grind.offset) pat (Lean.mkRawNatLit k)

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

Equations

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

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

Equations

• Lean.Meta.Grind.mkEqBwdPattern u α lhs rhs = Lean.mkApp3 (Lean.mkConst `Lean.Grind.eqBwdPattern u) α lhs rhs

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

Equations

• Lean.Meta.Grind.isEqBwdPattern e = e.isAppOfArity `Lean.Grind.eqBwdPattern 3

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

Equations

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

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

Equations

• Lean.Meta.Grind.mkGenPattern u α h x val = Lean.mkApp4 (Lean.mkConst `Lean.Grind.genPattern u) α h x val

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

Equations

• Lean.Meta.Grind.mkGenHEqPattern u α β h x val = Lean.mkApp5 (Lean.mkConst `Lean.Grind.genHEqPattern u) α β h x val

structure Lean.Meta.Grind.GenPatternInfo : Type

Generalized pattern information. See Grind.genPattern gadget.

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

def Lean.Meta.Grind.instReprGenPatternInfo.repr : GenPatternInfo → Nat → Format

Equations

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

@[implicit_reducible]

instance Lean.Meta.Grind.instReprGenPatternInfo : Repr GenPatternInfo

Equations

• Lean.Meta.Grind.instReprGenPatternInfo = { reprPrec := Lean.Meta.Grind.instReprGenPatternInfo.repr }

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

Equations

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

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

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

Equations

• Lean.Meta.Grind.isMatchCongrEqDeclName (p.str s) = (pure (Lean.Meta.Match.isCongrEqnReservedNameSuffix s) <&&> (Lean.Meta.isMatcher p <||> Lean.Meta.isMatcher (Lean.privateToUserName p)))
• Lean.Meta.Grind.isMatchCongrEqDeclName declName = pure false

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

Equations

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

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

Equations

• (Lean.Meta.Grind.EMatchTheoremKind.eqLhs gen).isEqLhs = true
• x✝.isEqLhs = false

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

Equations

• (Lean.Meta.Grind.EMatchTheoremKind.default gen).isDefault = true
• x✝.isDefault = false

def Lean.Meta.Grind.EMatchTheoremKind.toAttributeCore (kind : EMatchTheoremKind) : String

Equations

• (Lean.Meta.Grind.EMatchTheoremKind.eqLhs true).toAttributeCore = "= gen"
• (Lean.Meta.Grind.EMatchTheoremKind.eqLhs false).toAttributeCore = "="
• (Lean.Meta.Grind.EMatchTheoremKind.eqRhs true).toAttributeCore = "=_ gen"
• (Lean.Meta.Grind.EMatchTheoremKind.eqRhs false).toAttributeCore = "=_"
• (Lean.Meta.Grind.EMatchTheoremKind.eqBoth false).toAttributeCore = "_=_"
• (Lean.Meta.Grind.EMatchTheoremKind.eqBoth true).toAttributeCore = "_=_ gen"
• Lean.Meta.Grind.EMatchTheoremKind.eqBwd.toAttributeCore = "←="
• Lean.Meta.Grind.EMatchTheoremKind.fwd.toAttributeCore = "→"
• (Lean.Meta.Grind.EMatchTheoremKind.bwd false).toAttributeCore = "←"
• (Lean.Meta.Grind.EMatchTheoremKind.bwd true).toAttributeCore = "← gen"
• Lean.Meta.Grind.EMatchTheoremKind.leftRight.toAttributeCore = "=>"
• Lean.Meta.Grind.EMatchTheoremKind.rightLeft.toAttributeCore = "<="
• (Lean.Meta.Grind.EMatchTheoremKind.default false).toAttributeCore = "."
• (Lean.Meta.Grind.EMatchTheoremKind.default true).toAttributeCore = ". gen"
• Lean.Meta.Grind.EMatchTheoremKind.user.toAttributeCore = ""

def Lean.Meta.Grind.EMatchTheoremKind.toAttribute (k : EMatchTheoremKind) (minIndexable : Bool) : String

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Grind.EMatchTheorems : Type

Set of E-matching theorems.

Equations

• Lean.Meta.Grind.EMatchTheorems = Lean.Meta.Grind.Theorems Lean.Meta.Grind.EMatchTheorem

@[reducible, inline]

abbrev Lean.Meta.Grind.EMatchTheoremsArray : Type

A collection of sets of E-matching theorems.

Equations

• Lean.Meta.Grind.EMatchTheoremsArray = Lean.Meta.Grind.TheoremsArray Lean.Meta.Grind.EMatchTheorem

def Lean.Meta.Grind.EMatchTheorems.containsWithSamePatterns (s : EMatchTheorems) (origin : Origin) (patterns : List Expr) (cnstrs : List EMatchTheoremConstraint) : Bool

Returns true if there is a theorem with exactly the same pattern and constraints is already in s

Equations

• s.containsWithSamePatterns origin patterns cnstrs = (Lean.Meta.Grind.Theorems.find s origin).any fun (thm : Lean.Meta.Grind.EMatchTheorem) => thm.patterns == patterns && thm.cnstrs == cnstrs

def Lean.Meta.Grind.ExtensionStateArray.containsWithSamePatterns (s : ExtensionStateArray) (origin : Origin) (patterns : List Expr) (cnstrs : List EMatchTheoremConstraint) : Bool

Equations

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

def Lean.Meta.Grind.EMatchTheorems.getKindsFor (s : EMatchTheorems) (origin : Origin) : List EMatchTheoremKind

Equations

• s.getKindsFor origin = List.map (fun (x : Lean.Meta.Grind.EMatchTheorem) => x.kind) (Lean.Meta.Grind.Theorems.find s origin)

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

Equations

• thm.getProofWithFreshMVarLevels = Lean.Meta.Grind.getProofWithFreshMVarLevels thm

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

Equations

• Lean.Meta.Grind.mkGroundPattern e = Lean.mkAnnotation `grind.ground_pat e

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

Equations

• Lean.Meta.Grind.groundPattern? e = Lean.annotation? `grind.ground_pat e

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

Equations

• Lean.Meta.Grind.isPatternDontCare e = (e == Lean.Meta.Grind.dontCare✝)

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

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

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

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.

• outParam : PatternArgKind

  outParam arguments are uniquely determined by type class resolution and should not be part of the e-matching pattern. Including them is redundant (the instance, which is already wildcarded, determines the outParam value) and harmful when the normalizer changes their syntactic form.

  Motivation. Consider the ToInt class used by the grind linear arithmetic module:

  class ToInt (α : Type) (range : outParam IntInterval) where ...
  instance : ToInt (Fin n) (.co 0 n) where ...
  @[grind =] theorem toInt_fin (x : Fin n) : ToInt.toInt x = x.val
  

  The elaborated pattern for toInt_fin is:

  @ToInt.toInt (Fin #1) (IntInterval.co 0 (NatCast.natCast #1)) _ #0
  

  The range argument IntInterval.co 0 (NatCast.natCast #1) is included in the pattern because the pattern generator treats it as relevant. However, the grind normalizer pushes NatCast.natCast inside arithmetic operations, rewriting ↑(n + 1) to ↑n + 1. So when grind processes Fin (n + 1), the e-graph contains:

  @ToInt.toInt (Fin (n + 1)) (IntInterval.co 0 (↑n + 1)) inst x
  

  The pattern expects NatCast.natCast #1 at the second position of IntInterval.co, but the e-graph has HAdd.hAdd (NatCast.natCast n) 1 — a different head symbol. The pattern cannot match, and toInt_fin never fires.

  Since outParam arguments are determined by type class resolution (just like instance arguments, which are already wildcarded), they can be safely ignored in patterns. This is justified by the same reasoning: after e-matching finds candidate substitutions, the instantiation step checks all arguments via isDefEq, preserving soundness.

@[implicit_reducible]

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

Equations

• Lean.Meta.Grind.NormalizePattern.instReprPatternArgKind = { reprPrec := Lean.Meta.Grind.NormalizePattern.instReprPatternArgKind.repr }

def Lean.Meta.Grind.NormalizePattern.instReprPatternArgKind.repr : PatternArgKind → Nat → Format

Equations

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

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

Equations

• Lean.Meta.Grind.NormalizePattern.PatternArgKind.relevant.isSupport = false
• x✝.isSupport = true

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.

Equations

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

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

Equations

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

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) (cnstrs : List EMatchTheoremConstraint := []) (showInfo minIndexable : 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.

Equations

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

def Lean.Meta.Grind.mkEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) (kind : EMatchTheoremKind) (minIndexable : Bool) (cnstrs : List EMatchTheoremConstraint) : 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.

Equations

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

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.

Equations

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

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

Equations

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

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

Equations

• ext.isEMatchTheorem declName = do let __do_lift ← Lean.getEnv pure ((Lean.ScopedEnvExtension.getState ext __do_lift).ematch.contains (Lean.Meta.Grind.Origin.decl declName))

def Lean.Meta.Grind.Extension.getEMatchTheorems (ext : Extension) : CoreM EMatchTheorems

Equations

• ext.getEMatchTheorems = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState ext __do_lift).ematch

def Lean.Meta.Grind.Extension.getEMatchTheoremsForNamespace (ext : Extension) (namespaceName : Name) : CoreM (Array EMatchTheorem)

Returns the scoped E-matching theorems declared in the given namespace.

Equations

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

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.

Equations

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

def Lean.Meta.Grind.Extension.addEMatchTheorem (ext : Extension) (declName : Name) (numParams : Nat) (patterns : List Expr) (kind : EMatchTheoremKind) (minIndexable : Bool) (attrKind : AttributeKind := AttributeKind.global) (cnstrs : List EMatchTheoremConstraint) : MetaM Unit

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

Equations

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

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

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

Equations

• ext.addEMatchEqTheorem declName = do let __do_lift ← Lean.Meta.Grind.mkEMatchEqTheorem declName Lean.ScopedEnvExtension.add ext (Lean.Meta.Grind.Entry.ematch __do_lift)

opaque Lean.Meta.Grind.backward.grind.inferPattern : Lean.Option Bool

opaque Lean.Meta.Grind.backward.grind.checkInferPatternDiscrepancy : Lean.Option Bool

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

Equations

• (Lean.Meta.Grind.EMatchTheoremKind.eqLhs gen).gen = gen
• (Lean.Meta.Grind.EMatchTheoremKind.eqRhs gen).gen = gen
• (Lean.Meta.Grind.EMatchTheoremKind.eqBoth gen).gen = gen
• (Lean.Meta.Grind.EMatchTheoremKind.default gen).gen = gen
• (Lean.Meta.Grind.EMatchTheoremKind.bwd gen).gen = gen
• Lean.Meta.Grind.EMatchTheoremKind.eqBwd.gen = false
• Lean.Meta.Grind.EMatchTheoremKind.fwd.gen = false
• Lean.Meta.Grind.EMatchTheoremKind.rightLeft.gen = false
• Lean.Meta.Grind.EMatchTheoremKind.leftRight.gen = false
• Lean.Meta.Grind.EMatchTheoremKind.user.gen = false

def Lean.Meta.Grind.mkEMatchTheoremUsingSingletonPatterns (origin : Origin) (levelParams : Array Name) (proof : Expr) (minPrio : Nat) (symPrios : SymbolPriorities) (showInfo : Bool := false) : MetaM (Array EMatchTheorem)

Collects all singleton patterns in the type of the given proof. We use this function to implement local forall expressions in a grind goal.

Equations

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

def Lean.Meta.Grind.mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : EMatchTheoremKind) (symPrios : SymbolPriorities) (groundPatterns : Bool := true) (showInfo minIndexable : 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.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Meta.Grind.EMatchTheoremKind.toSyntax (kind : EMatchTheoremKind) : CoreM (TSyntax `Lean.Parser.Attr.grindMod)

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.EMatchTheoremKind.user.toSyntax = Lean.throwError (Lean.toMessageData "`grind` theorem kind is not a modifier")

opaque Lean.Meta.Grind.grind.param.codeAction : Lean.Option Bool

inductive Lean.Meta.Grind.MinIndexableMode : Type

Helper type for generating suggestions for grind parameters

• yes : MinIndexableMode

  minIndexable := true

• no : MinIndexableMode

  minIndexable := false

• both : MinIndexableMode

  Tries with and without the minimal indexable subexpression condition, if both produce the same pattern, use the one minIndexable := false since it is more compact.

def Lean.Meta.Grind.mkEMatchTheoremAndSuggest (ref : Syntax) (declName : Name) (prios : SymbolPriorities) (minIndexable : Bool) (isParam : Bool := false) : MetaM EMatchTheorem

Tries different modifiers, logs info messages with modifiers that worked, but returns just the first one that worked.

Equations

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

def Lean.Meta.Grind.Extension.addEMatchAttrAndSuggest (ext : Extension) (ref : Syntax) (declName : Name) (attrKind : AttributeKind) (prios : SymbolPriorities) (minIndexable showInfo : Bool) (isParam : Bool := false) : MetaM Unit

Tries different modifiers, logs info messages with modifiers that worked, but stores just the first one that worked.

Remark: if backward.grind.inferPattern is true, then .default false is used. The parameter showInfo is only taken into account when backward.grind.inferPattern is true.

Equations

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