structure Lean.Meta.Grind.InjectiveTheorem : Type

A theorem marked with @[grind inj]

• levelParams : Array Name
• proof : Expr
• symbols : List HeadIndex

  Contains all symbols used in the term f at the theorem's conclusion: Function.Injective f.

• origin : Origin

def Lean.Meta.Grind.instInhabitedInjectiveTheorem.default : InjectiveTheorem

Equations

• Lean.Meta.Grind.instInhabitedInjectiveTheorem.default = { levelParams := default, proof := default, symbols := default, origin := default }

instance Lean.Meta.Grind.instInhabitedInjectiveTheorem : Inhabited InjectiveTheorem

Equations

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

instance Lean.Meta.Grind.instTheoremLikeInjectiveTheorem : TheoremLike InjectiveTheorem

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Grind.InjectiveTheorems : Type

Set of Injective theorems.

Equations

• Lean.Meta.Grind.InjectiveTheorems = Lean.Meta.Grind.Theorems Lean.Meta.Grind.InjectiveTheorem

def Lean.Meta.Grind.mkInjectiveTheorem (declName : Name) : MetaM InjectiveTheorem

Equations

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

def Lean.Meta.Grind.addInjectiveAttr (declName : Name) (attrKind : AttributeKind) : MetaM Unit

Equations

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

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

Equations

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

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

Returns true if declName has been tagged as an injective theorem using [grind].

Equations

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

def Lean.Meta.Grind.getInjectiveTheorems : CoreM InjectiveTheorems

Returns the injective theorems registered in the environment.

Equations

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

def Lean.Meta.Grind.resetInjectiveTheoremsExt : CoreM Unit

Equations

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