Grind extensionality attribute to mark which [ext] theorems should be used.

@[reducible, inline]

abbrev Lean.Meta.Grind.ExtTheorems : Type

Extensionality theorems that can be used by grind

Equations

• Lean.Meta.Grind.ExtTheorems = Lean.PHashSet Lean.Name

opaque Lean.Meta.Grind.extTheoremsExt : SimpleScopedEnvExtension Name ExtTheorems

def Lean.Meta.Grind.validateExtAttr (declName : Name) : CoreM Unit

Equations

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

def Lean.Meta.Grind.addExtAttr (declName : Name) (attrKind : AttributeKind) : CoreM Unit

Equations

• Lean.Meta.Grind.addExtAttr declName attrKind = do Lean.Meta.Grind.validateExtAttr declName Lean.ScopedEnvExtension.add Lean.Meta.Grind.extTheoremsExt declName attrKind

def Lean.Meta.Grind.eraseExtAttr (declName : Name) : CoreM Unit

Equations

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

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

Equations

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