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

instance Lean.Meta.Grind.instInhabitedSymbolPriorityEntry : Inhabited SymbolPriorityEntry

Equations

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

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

Equations

• Lean.Meta.Grind.instInhabitedSymbolPriorityEntry.default = { declName := default, prio := 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

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

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

Equations

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

def Lean.Meta.Grind.instInhabitedOrigin.default : Origin

Equations

• Lean.Meta.Grind.instInhabitedOrigin.default = Lean.Meta.Grind.Origin.decl default

instance Lean.Meta.Grind.instReprOrigin : Repr Origin

Equations

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

def Lean.Meta.Grind.instReprOrigin.repr : Origin → Nat → Format

Equations

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

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

A unique identifier corresponding to the origin.

Equations

• (Lean.Meta.Grind.Origin.decl a).key = a
• (Lean.Meta.Grind.Origin.fvar a).key = a.name
• (Lean.Meta.Grind.Origin.stx a a_1).key = a
• (Lean.Meta.Grind.Origin.local a).key = a

def Lean.Meta.Grind.Origin.pp (o : Origin) : MessageData

Equations

• (Lean.Meta.Grind.Origin.decl a).pp = Lean.MessageData.ofConstName a
• (Lean.Meta.Grind.Origin.fvar a).pp = Lean.MessageData.ofExpr (Lean.mkFVar a)
• (Lean.Meta.Grind.Origin.stx a a_1).pp = Lean.MessageData.ofSyntax a_1
• (Lean.Meta.Grind.Origin.local a).pp = Lean.MessageData.ofName a

instance Lean.Meta.Grind.instBEqOrigin : BEq Origin

Equations

• Lean.Meta.Grind.instBEqOrigin = { beq := fun (a b : Lean.Meta.Grind.Origin) => a.key == b.key }

instance Lean.Meta.Grind.instHashableOrigin : Hashable Origin

Equations

• Lean.Meta.Grind.instHashableOrigin = { hash := fun (a : Lean.Meta.Grind.Origin) => hash a.key }

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 }

instance Lean.Meta.Grind.instBEqEMatchTheoremKind : BEq EMatchTheoremKind

Equations

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

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

Equations

• Lean.Meta.Grind.instBEqEMatchTheoremKind.beq (Lean.Meta.Grind.EMatchTheoremKind.eqLhs a) (Lean.Meta.Grind.EMatchTheoremKind.eqLhs b) = (a == b)
• Lean.Meta.Grind.instBEqEMatchTheoremKind.beq (Lean.Meta.Grind.EMatchTheoremKind.eqRhs a) (Lean.Meta.Grind.EMatchTheoremKind.eqRhs b) = (a == b)
• Lean.Meta.Grind.instBEqEMatchTheoremKind.beq (Lean.Meta.Grind.EMatchTheoremKind.eqBoth a) (Lean.Meta.Grind.EMatchTheoremKind.eqBoth b) = (a == b)
• Lean.Meta.Grind.instBEqEMatchTheoremKind.beq Lean.Meta.Grind.EMatchTheoremKind.eqBwd Lean.Meta.Grind.EMatchTheoremKind.eqBwd = true
• Lean.Meta.Grind.instBEqEMatchTheoremKind.beq Lean.Meta.Grind.EMatchTheoremKind.fwd Lean.Meta.Grind.EMatchTheoremKind.fwd = true
• Lean.Meta.Grind.instBEqEMatchTheoremKind.beq (Lean.Meta.Grind.EMatchTheoremKind.bwd a) (Lean.Meta.Grind.EMatchTheoremKind.bwd b) = (a == b)
• Lean.Meta.Grind.instBEqEMatchTheoremKind.beq Lean.Meta.Grind.EMatchTheoremKind.leftRight Lean.Meta.Grind.EMatchTheoremKind.leftRight = true
• Lean.Meta.Grind.instBEqEMatchTheoremKind.beq Lean.Meta.Grind.EMatchTheoremKind.rightLeft Lean.Meta.Grind.EMatchTheoremKind.rightLeft = true
• Lean.Meta.Grind.instBEqEMatchTheoremKind.beq (Lean.Meta.Grind.EMatchTheoremKind.default a) (Lean.Meta.Grind.EMatchTheoremKind.default b) = (a == b)
• Lean.Meta.Grind.instBEqEMatchTheoremKind.beq Lean.Meta.Grind.EMatchTheoremKind.user Lean.Meta.Grind.EMatchTheoremKind.user = true
• Lean.Meta.Grind.instBEqEMatchTheoremKind.beq x✝¹ x✝ = false

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 }

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

instance Lean.Meta.Grind.instHashableEMatchTheoremKind : Hashable EMatchTheoremKind

Equations

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

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.toAttribute : EMatchTheoremKind → String

Equations

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

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

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.

structure Lean.Meta.Grind.EMatchTheorems : Type

Set of E-matching theorems.

• smap : Lean.PHashMap Lean.Name (List Lean.Meta.Grind.EMatchTheorem)
• origins : Lean.PHashSet Lean.Meta.Grind.Origin
• erased : Lean.PHashSet Lean.Meta.Grind.Origin
• omap : Lean.PHashMap Lean.Meta.Grind.Origin (List Lean.Meta.Grind.EMatchTheorem)
• prios : Lean.Meta.Grind.SymbolPriorities

instance Lean.Meta.Grind.instInhabitedEMatchTheorems : Inhabited EMatchTheorems

Equations

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

def Lean.Meta.Grind.instInhabitedEMatchTheorems.default : EMatchTheorems

Equations

• Lean.Meta.Grind.instInhabitedEMatchTheorems.default = { smap := default, origins := default, erased := default, omap := default, prios := default }

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.

Equations

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

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

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

Equations

• s.contains origin = Lean.PersistentHashSet.contains (Lean.Meta.Grind.EMatchTheorems.origins✝ s) origin

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

Marks the theorem with the given origin as erased

Equations

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

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

Returns true if the theorem has been marked as erased.

Equations

• s.isErased origin = Lean.PersistentHashSet.contains (Lean.Meta.Grind.EMatchTheorems.erased✝ s) origin

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

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

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

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

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

Equations

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

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

Returns theorems associated with the given origin.

Equations

• s.find origin = match Lean.PersistentHashMap.find? (Lean.Meta.Grind.EMatchTheorems.omap✝ s) origin with | some thms => thms | x => []

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

Equations

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

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.

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

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) : 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) (attrKind : AttributeKind := AttributeKind.global) : 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.EMatchTheorems.getOrigins (s : EMatchTheorems) : List Origin

Equations

• s.getOrigins = Lean.PersistentHashSet.toList (Lean.Meta.Grind.EMatchTheorems.origins✝ s)

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 : 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 : 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 : Bool := false) : MetaM Unit

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.