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