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

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

Instances For

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

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

Instances For

source
instance Lean.Meta.Grind.instInhabitedOrigin :
Inhabited Origin
Equations

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

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

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

Instances For

source
instance Lean.Meta.Grind.instReprOrigin :
Repr Origin
Equations

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

source
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

Instances For

source
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

Instances For

source
instance Lean.Meta.Grind.instBEqOrigin :
BEq Origin
Equations

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

source
instance Lean.Meta.Grind.instHashableOrigin :
Hashable Origin
Equations

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

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

Instances For

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

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

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

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

Instances For

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

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

Instances

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

Instances For

source
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

Instances For

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

Instances For

source
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

Instances For

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

Instances For

source
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 => []

Instances For

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

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

Instances For

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

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

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

Instances For