A collection of theorems. We use it to implement E-matching and injectivity theorems used by grind.

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.

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

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedOrigin : Inhabited Origin

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

@[implicit_reducible]

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 (o : Origin) : MessageData

@[implicit_reducible]

instance Lean.Meta.Grind.instBEqOrigin : BEq Origin

@[implicit_reducible]

instance Lean.Meta.Grind.instHashableOrigin : Hashable Origin

structure Lean.Meta.Grind.Theorems (α : Type) : Type

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

def Lean.Meta.Grind.instInhabitedTheorems.default {a✝ : Type} : Theorems a✝

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedTheorems {a✝ : Type} : Inhabited (Theorems a✝)

class Lean.Meta.Grind.TheoremLike (α : Type) : Type

• getSymbols : α → List HeadIndex
• setSymbols : α → List HeadIndex → α
• getOrigin : α → Origin
• getProof : α → Expr
• getLevelParams : α → Array Name

def Lean.Meta.Grind.Theorems.insert {α : Type} [TheoremLike α] (s : Theorems α) (thm : α) : Theorems α

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.Theorems.contains {α : Type} (s : Theorems α) (origin : Origin) : Bool

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

def Lean.Meta.Grind.Theorems.erase {α : Type} (s : Theorems α) (origin : Origin) : Theorems α

Marks the theorem with the given origin as erased

def Lean.Meta.Grind.Theorems.isErased {α : Type} (s : Theorems α) (origin : Origin) : Bool

Returns true if the theorem has been marked as erased.

@[inline]

def Lean.Meta.Grind.Theorems.retrieve? {α : Type} (s : Theorems α) (sym : Name) : Option (List α × Theorems α)

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

def Lean.Meta.Grind.Theorems.find {α : Type} (s : Theorems α) (origin : Origin) : List α

Returns theorems associated with the given origin.

def Lean.Meta.Grind.getProofWithFreshMVarLevels {α : Type} [TheoremLike α] (thm : α) : MetaM Expr

def Lean.Meta.Grind.Theorems.eraseDecl {α : Type} (s : Theorems α) (declName : Name) : MetaM (Theorems α)

def Lean.Meta.Grind.Theorems.getOrigins {α : Type} (s : Theorems α) : List Origin

def Lean.Meta.Grind.Theorems.mkEmpty (α : Type) : Theorems α

@[implicit_reducible]

instance Lean.Meta.Grind.instEmptyCollectionTheorems {α : Type} : EmptyCollection (Theorems α)

def Lean.Meta.Grind.getProofForDecl (declName : Name) : MetaM Expr

@[reducible, inline]

abbrev Lean.Meta.Grind.TheoremsArray (α : Type) : Type

A TheoremsArray α is a collection of Theorems α. The array is scanned linear during theorem activation. This avoids the need for efficiently merging the Theorems α data structure.

@[specialize #[]]

def Lean.Meta.Grind.TheoremsArray.retrieve? {α : Type} (s : TheoremsArray α) (sym : Name) : Option (List α × TheoremsArray α)

def Lean.Meta.Grind.TheoremsArray.insert {α : Type} [TheoremLike α] (s : TheoremsArray α) (thm : α) : TheoremsArray α

def Lean.Meta.Grind.TheoremsArray.isErased {α : Type} (s : TheoremsArray α) (origin : Origin) : Bool

def Lean.Meta.Grind.TheoremsArray.find {α : Type} (s : TheoremsArray α) (origin : Origin) : List α