structure Aesop.TraceOption : Type

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

instance Aesop.instInhabitedTraceOption : Inhabited TraceOption

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

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

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

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

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

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

def Aesop.ruleSuccessEmoji : String

def Aesop.ruleFailureEmoji : String

def Aesop.ruleProvedEmoji : String

def Aesop.ruleErrorEmoji : String

def Aesop.rulePostponedEmoji : String

def Aesop.ruleSkippedEmoji : String

def Aesop.nodeUnknownEmoji : String

def Aesop.nodeProvedEmoji : String

def Aesop.nodeUnprovableEmoji : String

def Aesop.newNodeEmoji : String

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

@[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} (opt : TraceOption) (msg : Except ε α → m Lean.MessageData) (k : m α) (collapsed : Bool := true) : m α

@[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.ExceptToEmoji ε α] (opt : TraceOption) (msg : m Lean.MessageData) (k : m α) (collapsed : Bool := true) : m α

@[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} (opt : TraceOption) (msg : m Lean.MessageData) (k : m α) (collapsed : Bool := true) : m α

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

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