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

Equations

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

def Aesop.Goal.withHeadlineTraceNode.fmt (g : Aesop.Goal) (transform : optParam (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 : Aesop.Goal) (traceOpt : Aesop.TraceOption) : Lean.MetaM Unit

Equations

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

def Aesop.Goal.traceMetadata.trc (traceOpt : Aesop.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 : Aesop.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 true

def Aesop.Rapp.withHeadlineTraceNode {α : Type} (r : Aesop.Rapp) (traceOpt : Aesop.TraceOption) (k : Lean.MetaM α) (collapsed : optParam Bool true) (transform : optParam (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 : Aesop.Rapp) (traceOpt : Aesop.TraceOption) : Lean.MetaM Unit

Equations

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

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

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

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

Equations

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

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

Equations

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