opaque Lean.PremiseSelection.moduleDenyListExt : SimplePersistentEnvExtension String (List String)

Premises from a module whose name has one of the following components are not retrieved.

opaque Lean.PremiseSelection.nameDenyListExt : SimplePersistentEnvExtension String (List String)

A premise whose name has one of the following components is not retrieved.

opaque Lean.PremiseSelection.typePrefixDenyListExt : SimplePersistentEnvExtension Name (List Name)

A premise whose type.getForallBody.getAppFn is a constant that has one of these prefixes is not retrieved.

def Lean.PremiseSelection.isDeniedModule (env : Environment) (moduleName : Name) : Bool

Equations

• Lean.PremiseSelection.isDeniedModule env moduleName = (Lean.PremiseSelection.moduleDenyListExt.getState env).any fun (p : String) => moduleName.anyS fun (x : String) => x == p

def Lean.PremiseSelection.isDeniedPremise (env : Environment) (name : Name) : Bool

Equations

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