Documentation

Aesop.Tree.Tracing

source
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 α
Instances For
    source
    def Aesop.Goal.traceMetadata (g : Goal) (traceOpt : TraceOption) :
    Lean.MetaM Unit
    Instances For
      source
      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 α
      Instances For
        source
        def Aesop.Rapp.traceMetadata (r : Rapp) (traceOpt : TraceOption) :
        Lean.MetaM Unit
        Instances For
          source
          partial def Aesop.Goal.traceTreeCore (g : Goal) (traceOpt : TraceOption) :
          Lean.MetaM Unit
          source
          partial def Aesop.Rapp.traceTreeCore (r : Rapp) (traceOpt : TraceOption) :
          Lean.MetaM Unit
          source
          def Aesop.Goal.traceTree (g : Goal) (traceOpt : TraceOption) :
          Lean.MetaM Unit
          Instances For
            source
            def Aesop.Rapp.traceTree (r : Rapp) (traceOpt : TraceOption) :
            Lean.MetaM Unit
            Instances For