structure Aesop.TraceOption : Type

• traceClass : Lean.Name
• option : Lean.Option Bool

def Aesop.instInhabitedTraceOption.default : TraceOption

Equations

• Aesop.instInhabitedTraceOption.default = { traceClass := default, option := default }

@[implicit_reducible]

instance Aesop.instInhabitedTraceOption : Inhabited TraceOption

Equations

• Aesop.instInhabitedTraceOption = { default := Aesop.instInhabitedTraceOption.default }

def Aesop.registerTraceOption (traceName : Lean.Name) (descr : String) : IO TraceOption

Equations

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

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

Equations

• opt.isEnabled = do let __do_lift ← Lean.getOptions pure (Lean.Option.get __do_lift opt.option)

def Aesop.TraceOption.withEnabled {m : Type → Type} {α : Type} [Lean.MonadWithOptions m] (opt : TraceOption) (k : m α) : m α

Equations

• opt.withEnabled k = Lean.withOptions (fun (opts : Lean.Options) => Lean.Option.set opts opt.option true) k

opaque Aesop.TraceOption.steps : TraceOption

opaque Aesop.TraceOption.ruleSet : TraceOption

opaque Aesop.TraceOption.proof : TraceOption

opaque Aesop.TraceOption.tree : TraceOption

opaque Aesop.TraceOption.extraction : TraceOption

opaque Aesop.TraceOption.stats : TraceOption

opaque Aesop.TraceOption.debug : TraceOption

opaque Aesop.TraceOption.script : TraceOption

opaque Aesop.TraceOption.forward : TraceOption

opaque Aesop.TraceOption.forwardDebug : TraceOption

opaque Aesop.TraceOption.rpinf : TraceOption

def Aesop.resolveTraceOption (stx : Lean.Ident) : Lean.MacroM Lean.Name

Equations

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

def Aesop.«doElemAesop_trace![_]__» : Lean.ParserDescr

Equations

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

def Aesop.«doElemAesop_trace[_]___» : Lean.ParserDescr

Equations

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

def Aesop.ruleSuccessEmoji : String

Equations

• Aesop.ruleSuccessEmoji = Lean.checkEmoji

def Aesop.ruleFailureEmoji : String

Equations

• Aesop.ruleFailureEmoji = Lean.crossEmoji

def Aesop.ruleProvedEmoji : String

Equations

• Aesop.ruleProvedEmoji = "🏁"

def Aesop.ruleErrorEmoji : String

Equations

• Aesop.ruleErrorEmoji = Lean.bombEmoji

def Aesop.rulePostponedEmoji : String

Equations

• Aesop.rulePostponedEmoji = "⏳️"

def Aesop.ruleSkippedEmoji : String

Equations

• Aesop.ruleSkippedEmoji = "⏩️"

def Aesop.nodeUnknownEmoji : String

Equations

• Aesop.nodeUnknownEmoji = "❓️"

def Aesop.nodeProvedEmoji : String

Equations

• Aesop.nodeProvedEmoji = Aesop.ruleProvedEmoji

def Aesop.nodeUnprovableEmoji : String

Equations

• Aesop.nodeUnprovableEmoji = Aesop.ruleFailureEmoji

def Aesop.newNodeEmoji : String

Equations

• Aesop.newNodeEmoji = "🆕"

def Aesop.exceptRuleResultToEmoji {α : Type u_1} {ε : Type u_2} (toEmoji : α → String) : Except ε α → String

Equations

• Aesop.exceptRuleResultToEmoji toEmoji (Except.error a) = Aesop.ruleFailureEmoji
• Aesop.exceptRuleResultToEmoji toEmoji (Except.ok r) = toEmoji r

@[always_inline]

def Aesop.withAesopTraceNode {m : Type → Type} {ε : Type} [Monad m] [Lean.MonadTrace m] [MonadLiftT BaseIO m] [Lean.MonadRef m] [Lean.AddMessageContext m] [Lean.MonadOptions m] [Lean.MonadAlwaysExcept ε m] {α : Type} [Lean.ExceptToTraceResult ε α] (opt : TraceOption) (msg : Except ε α → m Lean.MessageData) (k : m α) (collapsed : Bool := true) : m α

Equations

• Aesop.withAesopTraceNode opt msg k collapsed = Lean.withTraceNode opt.traceClass msg k collapsed

@[always_inline]

def Aesop.withAesopTraceNodeBefore {m : Type → Type} {ε : Type} [Monad m] [Lean.MonadTrace m] [MonadLiftT BaseIO m] [Lean.MonadRef m] [Lean.AddMessageContext m] [Lean.MonadOptions m] [Lean.MonadAlwaysExcept ε m] {α : Type} [Lean.ExceptToTraceResult ε α] (opt : TraceOption) (msg : m Lean.MessageData) (k : m α) (collapsed : Bool := true) : m α

Equations

• Aesop.withAesopTraceNodeBefore opt msg k collapsed = Lean.withTraceNodeBefore opt.traceClass (fun (x : Unit) => msg) k collapsed

@[always_inline]

def Aesop.withConstAesopTraceNode {m : Type → Type} {ε : Type} [Monad m] [Lean.MonadTrace m] [MonadLiftT BaseIO m] [Lean.MonadRef m] [Lean.AddMessageContext m] [Lean.MonadOptions m] [Lean.MonadAlwaysExcept ε m] {α : Type} [Lean.ExceptToTraceResult ε α] (opt : TraceOption) (msg : m Lean.MessageData) (k : m α) (collapsed : Bool := true) : m α

Equations

• Aesop.withConstAesopTraceNode opt msg k collapsed = Aesop.withAesopTraceNode opt (fun (x : Except ε α) => msg) k collapsed

def Aesop.traceSimpTheoremTreeContents (t : Lean.Meta.SimpTheoremTree) (opt : TraceOption) : Lean.CoreM Unit

Equations

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

def Aesop.traceSimpTheorems (s : Lean.Meta.SimpTheorems) (opt : TraceOption) : Lean.CoreM Unit

Equations

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