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

Equations

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

def Lean.Meta.Grind.instInhabitedSymbolPriorities.default : SymbolPriorities

Equations

• Lean.Meta.Grind.instInhabitedSymbolPriorities.default = { map := default }

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 }

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.insert (s : SymbolPriorities) (declName : Name) (prio : Nat) : SymbolPriorities

Inserts declName ↦ prio into s.

Equations

• s.insert declName prio = { map := Lean.PersistentHashMap.insert s.map declName prio }

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.

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.

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

def Lean.Meta.Grind.instInhabitedEMatchTheoremKind.default : EMatchTheoremKind

Equations

• Lean.Meta.Grind.instInhabitedEMatchTheoremKind.default = Lean.Meta.Grind.EMatchTheoremKind.eqLhs default

instance Lean.Meta.Grind.instInhabitedEMatchTheoremKind : Inhabited EMatchTheoremKind

Equations

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

def Lean.Meta.Grind.instBEqEMatchTheoremKind.beq : EMatchTheoremKind → EMatchTheoremKind → Bool

Equations

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

instance Lean.Meta.Grind.instBEqEMatchTheoremKind : BEq EMatchTheoremKind

Equations

• Lean.Meta.Grind.instBEqEMatchTheoremKind = { beq := Lean.Meta.Grind.instBEqEMatchTheoremKind.beq }

def Lean.Meta.Grind.instReprEMatchTheoremKind.repr : EMatchTheoremKind → Nat → Format

Equations

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

instance Lean.Meta.Grind.instReprEMatchTheoremKind : Repr EMatchTheoremKind

Equations

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

instance Lean.Meta.Grind.instHashableEMatchTheoremKind : Hashable EMatchTheoremKind

Equations

• Lean.Meta.Grind.instHashableEMatchTheoremKind = { hash := Lean.Meta.Grind.instHashableEMatchTheoremKind.hash }

def Lean.Meta.Grind.instHashableEMatchTheoremKind.hash : EMatchTheoremKind → UInt64

Equations

• Lean.Meta.Grind.instHashableEMatchTheoremKind.hash (Lean.Meta.Grind.EMatchTheoremKind.eqLhs a) = mixHash 0 (hash a)
• Lean.Meta.Grind.instHashableEMatchTheoremKind.hash (Lean.Meta.Grind.EMatchTheoremKind.eqRhs a) = mixHash 1 (hash a)
• Lean.Meta.Grind.instHashableEMatchTheoremKind.hash (Lean.Meta.Grind.EMatchTheoremKind.eqBoth a) = mixHash 2 (hash a)
• Lean.Meta.Grind.instHashableEMatchTheoremKind.hash Lean.Meta.Grind.EMatchTheoremKind.eqBwd = 3
• Lean.Meta.Grind.instHashableEMatchTheoremKind.hash Lean.Meta.Grind.EMatchTheoremKind.fwd = 4
• Lean.Meta.Grind.instHashableEMatchTheoremKind.hash (Lean.Meta.Grind.EMatchTheoremKind.bwd a) = mixHash 5 (hash a)
• Lean.Meta.Grind.instHashableEMatchTheoremKind.hash Lean.Meta.Grind.EMatchTheoremKind.leftRight = 6
• Lean.Meta.Grind.instHashableEMatchTheoremKind.hash Lean.Meta.Grind.EMatchTheoremKind.rightLeft = 7
• Lean.Meta.Grind.instHashableEMatchTheoremKind.hash (Lean.Meta.Grind.EMatchTheoremKind.default a) = mixHash 8 (hash a)
• Lean.Meta.Grind.instHashableEMatchTheoremKind.hash Lean.Meta.Grind.EMatchTheoremKind.user = 9

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.

structure Lean.Meta.Grind.CnstrRHS : Type

• levelNames : Array Name

  Abstracted universe level param names in the rhs

• numMVars : Nat

  Number of abstracted metavariable in the rhs

• expr : Expr

  The actual rhs.

def Lean.Meta.Grind.instInhabitedCnstrRHS.default : CnstrRHS

Equations

• Lean.Meta.Grind.instInhabitedCnstrRHS.default = { levelNames := default, numMVars := default, expr := default }

instance Lean.Meta.Grind.instInhabitedCnstrRHS : Inhabited CnstrRHS

Equations

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

instance Lean.Meta.Grind.instBEqCnstrRHS : BEq CnstrRHS

Equations

• Lean.Meta.Grind.instBEqCnstrRHS = { beq := Lean.Meta.Grind.instBEqCnstrRHS.beq }

def Lean.Meta.Grind.instBEqCnstrRHS.beq : CnstrRHS → CnstrRHS → Bool

Equations

• Lean.Meta.Grind.instBEqCnstrRHS.beq { levelNames := a, numMVars := a_1, expr := a_2 } { levelNames := b, numMVars := b_1, expr := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Lean.Meta.Grind.instBEqCnstrRHS.beq x✝¹ x✝ = false

def Lean.Meta.Grind.instReprCnstrRHS.repr : CnstrRHS → Nat → Format

Equations

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

instance Lean.Meta.Grind.instReprCnstrRHS : Repr CnstrRHS

Equations

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

inductive Lean.Meta.Grind.EMatchTheoremConstraint : Type

Grind patterns may have constraints associated with them.

• notDefEq (lhs : Nat) (rhs : CnstrRHS) : EMatchTheoremConstraint

  A constraint of the form lhs =/= rhs. The lhs is one of the bound variables, and the rhs an abstract term that must not be definitionally equal to a term t assigned to lhs.

• defEq (lhs : Nat) (rhs : CnstrRHS) : EMatchTheoremConstraint

  A constraint of the form lhs =?= rhs. The lhs is one of the bound variables, and the rhs an abstract term that must be definitionally equal to a term t assigned to lhs.

• sizeLt (lhs n : Nat) : EMatchTheoremConstraint

  A constraint of the form size lhs < n. The lhs is one of the bound variables. The size is computed ignoring implicit terms, but sharing is not taken into account.

• depthLt (lhs n : Nat) : EMatchTheoremConstraint

  A constraint of the form depth lhs < n. The lhs is one of the bound variables. The depth is computed in constant time using the approxDepth field attached to expressions.

• genLt (n : Nat) : EMatchTheoremConstraint

  Instantiates the theorem only if its generation is less than n

• isGround (bvarIdx : Nat) : EMatchTheoremConstraint

  Constraints of the form is_ground x. Instantiates the theorem only if x is ground term.

• isValue (bvarIdx : Nat) (strict : Bool) : EMatchTheoremConstraint

  Constraints of the form is_value x and is_strict_value x. A value is defined as

  • A constructor fully applied to value arguments.
  • A literal: numerals, strings, etc.
  • A lambda. In the strict case, lambdas are not considered.
• maxInsts (n : Nat) : EMatchTheoremConstraint

  Instantiates the theorem only if less than n instances have been generated for this theorem.

• guard (e : Expr) : EMatchTheoremConstraint

  It instructs grind to postpone the instantiation of the theorem until e is known to be true.

• check (e : Expr) : EMatchTheoremConstraint

  Similar to guard, but checks whether e is implied by asserting ¬e.

• notValue (bvarIdx : Nat) (strict : Bool) : EMatchTheoremConstraint

  Constraints of the form not_value x and not_strict_value x. They are the negations of is_value x and is_strict_value x.

def Lean.Meta.Grind.instInhabitedEMatchTheoremConstraint.default : EMatchTheoremConstraint

Equations

• Lean.Meta.Grind.instInhabitedEMatchTheoremConstraint.default = Lean.Meta.Grind.EMatchTheoremConstraint.notDefEq default default

instance Lean.Meta.Grind.instInhabitedEMatchTheoremConstraint : Inhabited EMatchTheoremConstraint

Equations

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

def Lean.Meta.Grind.instReprEMatchTheoremConstraint.repr : EMatchTheoremConstraint → Nat → Format

Equations

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

instance Lean.Meta.Grind.instReprEMatchTheoremConstraint : Repr EMatchTheoremConstraint

Equations

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

def Lean.Meta.Grind.instBEqEMatchTheoremConstraint.beq : EMatchTheoremConstraint → EMatchTheoremConstraint → Bool

Equations

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

instance Lean.Meta.Grind.instBEqEMatchTheoremConstraint : BEq EMatchTheoremConstraint

Equations

• Lean.Meta.Grind.instBEqEMatchTheoremConstraint = { beq := Lean.Meta.Grind.instBEqEMatchTheoremConstraint.beq }

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?.

• minIndexable : Bool

  Stores whether patterns were inferred using the minimal indexable subexpression condition.

• cnstrs : List EMatchTheoremConstraint

instance Lean.Meta.Grind.instInhabitedEMatchTheorem : Inhabited EMatchTheorem

Equations

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

def Lean.Meta.Grind.instInhabitedEMatchTheorem.default : EMatchTheorem

Equations

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

instance Lean.Meta.Grind.instTheoremLikeEMatchTheorem : TheoremLike EMatchTheorem

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

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.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

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

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

Equations

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

def Lean.Meta.Grind.resetEMatchTheoremsExt : CoreM Unit

Equations

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

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.

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

Equations

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

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.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.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.addEMatchTheorem (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.addEMatchEqTheorem (declName : Name) : MetaM Unit

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

Equations

• Lean.Meta.Grind.addEMatchEqTheorem declName = do let __do_lift ← Lean.Meta.Grind.mkEMatchEqTheorem declName Lean.ScopedEnvExtension.add Lean.Meta.Grind.ematchTheoremsExt✝ __do_lift

def Lean.Meta.Grind.getEMatchTheorems : CoreM EMatchTheorems

Returns the E-matching theorems registered in the environment.

Equations

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

def Lean.Meta.Grind.getEMatchTheoremsForNamespace (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.

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.addEMatchAttr (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.addEMatchAttrAndSuggest (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.

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

Equations

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