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

Equations

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

instance Lean.Meta.Grind.instInhabitedOrigin : Inhabited Origin

Equations

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

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

Equations

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

instance Lean.Meta.Grind.instReprOrigin : Repr Origin

Equations

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

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 }

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 α)

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

Equations

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

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

Equations

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

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.

Equations

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

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

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

Equations

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

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

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

Returns true if the theorem has been marked as erased.

Equations

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

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

Equations

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

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

Returns theorems associated with the given origin.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Meta.Grind.Theorems.mkEmpty α = { }

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

Equations

• Lean.Meta.Grind.instEmptyCollectionTheorems = { emptyCollection := Lean.Meta.Grind.Theorems.mkEmpty α }

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

Equations

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