def EvalAuto.Name.getConstsOfModule (module : Lean.Name) : Lean.CoreM (Array Lean.Name)

Equations

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

def EvalAuto.tallyNamesByModule (names : Array Lean.Name) : Lean.CoreM (Std.HashMap Lean.Name (Array Lean.Name))

Equations

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

def EvalAuto.Name.getCi (name parentFunc : Lean.Name) : Lean.CoreM Lean.ConstantInfo

Used as a wrapper in other functions

Equations

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

def EvalAuto.Name.hasValue (name parentFunc : Lean.Name) : Lean.CoreM Bool

Used as a wrapper in other functions

Equations

• EvalAuto.Name.hasValue name parentFunc = do let __do_lift ← EvalAuto.Name.getCi name parentFunc pure __do_lift.value?.isSome

def EvalAuto.Name.getValue (name parentFunc : Lean.Name) : Lean.CoreM Lean.Expr

Used as a wrapper in other functions

Equations

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

def EvalAuto.Name.isTheorem (name : Lean.Name) : Lean.CoreM Bool

Equations

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

def EvalAuto.Name.isHumanTheorem (name : Lean.Name) : Lean.CoreM Bool

A constant is a human theorem iff it is a theorem and has a declaration range. Roughly speaking, a constant have a declaration range iff it is defined (presumably by a human) in a .lean file

Equations

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

def EvalAuto.allHumanTheorems : Lean.CoreM (Array Lean.Name)

Equations

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

def EvalAuto.Name.isFromPackage (name : Lean.Name) (pkgPrefix : String) : Lean.CoreM Bool

Equations

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

def EvalAuto.allHumanTheoremsFromPackage (pkgPrefix : String) : Lean.CoreM (Array Lean.Name)

Equations

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

def EvalAuto.Expr.getUsedTheorems (e : Lean.Expr) : Lean.CoreM (Array Lean.Name)

Return the theorems that occurs in an expression

Equations

• EvalAuto.Expr.getUsedTheorems e = Array.filterM EvalAuto.Name.isTheorem e.getUsedConstants

def EvalAuto.Name.getUsedTheorems (name : Lean.Name) : Lean.CoreM (Array Lean.Name)

Return the theorems that are used in the declaration body of a constant

Equations

• EvalAuto.Name.getUsedTheorems name = do let v ← EvalAuto.Name.getValue name `EvalAuto.Name.getUsedTheorems EvalAuto.Expr.getUsedTheorems v

def EvalAuto.Expr.onlyUsesConsts (e : Lean.Expr) (names : Array Lean.Name) : Bool

Return true if the expression e only uses constants present in names

Equations

• EvalAuto.Expr.onlyUsesConsts e names = e.getUsedConstants.all fun (name : Lean.Name) => names.contains name

def EvalAuto.Name.onlyUsesConsts (name : Lean.Name) (names : Array Lean.Name) : Lean.CoreM Bool

Return true if the declaration body of name only uses constants present in names

Equations

• EvalAuto.Name.onlyUsesConsts name names = do let v ← EvalAuto.Name.getValue name `EvalAuto.Name.onlyUsesConsts pure (EvalAuto.Expr.onlyUsesConsts v names)

def EvalAuto.Name.onlyUsesConstsInType (name : Lean.Name) (names : Array Lean.Name) : Lean.CoreM Bool

Return true if the type name only uses constants present in names

Equations

• EvalAuto.Name.onlyUsesConstsInType name names = do let ci ← EvalAuto.Name.getCi name `EvalAuto.Name.onlyUsesConstsInType pure (EvalAuto.Expr.onlyUsesConsts ci.type names)

def EvalAuto.logicConsts : Array Lean.Name

Used to filter out theorems known to SMT solvers and native provers

Equations

• EvalAuto.logicConsts = #[`True, `False, `Not, `And, `Or, `Iff, `Eq]

def EvalAuto.boolConsts : Array Lean.Name

Used to filter out theorems known to SMT solvers

Equations

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

def EvalAuto.natConsts : Array Lean.Name

Used to filter out theorems known to SMT solvers

Equations

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

def EvalAuto.Name.onlyLogicInType (name : Lean.Name) : Lean.CoreM Bool

Equations

• EvalAuto.Name.onlyLogicInType name = EvalAuto.Name.onlyUsesConstsInType name EvalAuto.logicConsts

def EvalAuto.Name.onlyBoolLogicInType (name : Lean.Name) : Lean.CoreM Bool

Equations

• EvalAuto.Name.onlyBoolLogicInType name = EvalAuto.Name.onlyUsesConstsInType name (EvalAuto.logicConsts ++ EvalAuto.boolConsts)

def EvalAuto.Name.onlyNatBoolLogicInType (name : Lean.Name) : Lean.CoreM Bool

Equations

• EvalAuto.Name.onlyNatBoolLogicInType name = EvalAuto.Name.onlyUsesConstsInType name (EvalAuto.logicConsts ++ EvalAuto.boolConsts ++ EvalAuto.natConsts)

def EvalAuto.analyze : Lean.CoreM (Array (Array Lean.Name))

Obtain Logic, Bool and Nat theorems

Equations

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