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.withHeadlineTraceNode.fmt (g : Goal) (transform : Lean.MessageData → Lean.MetaM Lean.MessageData := pure) : Lean.MetaM Lean.MessageData

Equations

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

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.Goal.traceMetadata.trc (traceOpt : TraceOption) (msg : Lean.MessageData) : Lean.MetaM Unit

Equations

• Aesop.Goal.traceMetadata.trc traceOpt msg = Lean.addTrace traceOpt.traceClass (Lean.toMessageData msg)

def Aesop.Goal.traceMetadata.trcNode (traceOpt : TraceOption) (msg : Lean.MessageData) (k : Lean.MetaM Unit) : Lean.MetaM Unit

Equations

• Aesop.Goal.traceMetadata.trcNode traceOpt msg k = Aesop.withConstAesopTraceNode traceOpt (pure msg) k

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.

def Aesop.Rapp.traceMetadata.trc (traceOpt : TraceOption) (m : Lean.MessageData) : Lean.MetaM Unit

Equations

• Aesop.Rapp.traceMetadata.trc traceOpt m = Lean.addTrace traceOpt.traceClass (Lean.toMessageData m)

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