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

@[reducible, inline]

abbrev Lean.Meta.Grind.InjectiveTheoremsArray : Type

A collections of sets of Injective theorems.

Equations

• Lean.Meta.Grind.InjectiveTheoremsArray = Lean.Meta.Grind.TheoremsArray 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.Extension.addInjectiveAttr (ext : Extension) (declName : Name) (attrKind : AttributeKind) : MetaM Unit

Equations

• ext.addInjectiveAttr declName attrKind = do let __do_lift ← Lean.Meta.Grind.mkInjectiveTheorem declName Lean.ScopedEnvExtension.add ext (Lean.Meta.Grind.Entry.inj __do_lift) attrKind