def Aesop.registerCheckOption (checkName : Lean.Name) (defValue : Bool) (descr : String) : IO (Lean.Option Bool)

Equations

• Aesop.registerCheckOption checkName defValue descr = Lean.Option.register (`aesop.check ++ checkName) { defValue := defValue, group := "aesop", descr := descr }

opaque Aesop.checkAllOption : Lean.Option Bool

opaque Aesop.checkProofReconstructionOption : Lean.Option Bool

opaque Aesop.checkTreeOption : Lean.Option Bool

opaque Aesop.checkUnificationGoalAssignmentsOption : Lean.Option Bool

opaque Aesop.checkRulesOption : Lean.Option Bool

opaque Aesop.checkScriptOption : Lean.Option Bool

opaque Aesop.checkScriptStepsOption : Lean.Option Bool

inductive Aesop.Check : Type

• all: Aesop.Check
• tree: Aesop.Check
• proofReconstruction: Aesop.Check
• unificationGoalAssignments: Aesop.Check
• rules: Aesop.Check
• script: Aesop.Check
• scriptSteps: Aesop.Check

@[inline_if_reduce]

def Aesop.Check.toOption : Aesop.Check → Lean.Option Bool

Equations

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

def Aesop.Check.isEnabled {m : Type → Type} [Monad m] [Lean.MonadOptions m] : Aesop.Check → m Bool

Equations

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

def Aesop.Check.name (c : Aesop.Check) : Lean.Name

Equations

• Aesop.Check.name c = (Aesop.Check.toOption c).name