opaque Aesop.Check.all : Lean.Option Bool

structure Aesop.Check : Type

• toOption : Lean.Option Bool

def Aesop.Check.get (opts : Lean.Options) (opt : Aesop.Check) : Bool

Equations

• Aesop.Check.get opts opt = match Lean.Option.get? opts opt.toOption with | some val => val | x => Lean.Option.get opts Aesop.Check.all

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

Equations

• Aesop.Check.isEnabled opt = do let __do_lift ← Lean.getOptions pure (Aesop.Check.get __do_lift opt)

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

Equations

• Aesop.Check.name opt = opt.toOption.name

def Aesop.Check.proofReconstruction : Aesop.Check

Equations

• Aesop.Check.proofReconstruction = { toOption := Aesop.option✝ }

def Aesop.Check.tree : Aesop.Check

Equations

• Aesop.Check.tree = { toOption := Aesop.option✝ }

def Aesop.Check.rules : Aesop.Check

Equations

• Aesop.Check.rules = { toOption := Aesop.option✝ }

def Aesop.Check.script : Aesop.Check

Equations

• Aesop.Check.script = { toOption := Aesop.option✝ }

def Aesop.Check.script.steps : Aesop.Check

Equations

• Aesop.Check.script.steps = { toOption := Aesop.option✝ }