def Aesop.Goal.withHeadlineTraceNode {α : Type} (g : Goal) (traceOpt : TraceOption) (k : Lean.MetaM α) (collapsed : Bool := true) (transform : Lean.MessageData → Lean.MetaM Lean.MessageData := pure) : Lean.MetaM α

Equations

• g.withHeadlineTraceNode traceOpt k collapsed transform = Aesop.withConstAesopTraceNode traceOpt (Aesop.Goal.withHeadlineTraceNode.fmt✝ g transform) k collapsed

def Aesop.Goal.traceMetadata (g : Goal) (traceOpt : TraceOption) : Lean.MetaM Unit

Equations

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

def Aesop.Rapp.withHeadlineTraceNode {α : Type} (r : Rapp) (traceOpt : TraceOption) (k : Lean.MetaM α) (collapsed : Bool := true) (transform : Lean.MessageData → Lean.MetaM Lean.MessageData := pure) : Lean.MetaM α

Equations

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

def Aesop.Rapp.traceMetadata (r : Rapp) (traceOpt : TraceOption) : Lean.MetaM Unit

Equations

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

partial def Aesop.Goal.traceTreeCore (g : Goal) (traceOpt : TraceOption) : Lean.MetaM Unit

partial def Aesop.Rapp.traceTreeCore (r : Rapp) (traceOpt : TraceOption) : Lean.MetaM Unit

def Aesop.Goal.traceTree (g : Goal) (traceOpt : TraceOption) : Lean.MetaM Unit

Equations

• g.traceTree traceOpt = do let __do_lift ← traceOpt.isEnabled if __do_lift = true then g.traceTreeCore traceOpt else pure PUnit.unit

def Aesop.Rapp.traceTree (r : Rapp) (traceOpt : TraceOption) : Lean.MetaM Unit

Equations

• r.traceTree traceOpt = do let __do_lift ← traceOpt.isEnabled if __do_lift = true then r.traceTreeCore traceOpt else pure PUnit.unit