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.withHeadlineTraceNode.fmt (g : Goal) (transform : Lean.MessageData → Lean.MetaM Lean.MessageData := pure) :
      Lean.MetaM Lean.MessageData
      Equations
        Instances For
          source
          def Aesop.Goal.traceMetadata (g : Goal) (traceOpt : TraceOption) :
          Lean.MetaM Unit
          Equations
            Instances For
              source
              def Aesop.Goal.traceMetadata.trc (traceOpt : TraceOption) (msg : Lean.MessageData) :
              Lean.MetaM Unit
              Equations
                Instances For
                  source
                  def Aesop.Goal.traceMetadata.trcNode (traceOpt : TraceOption) (msg : Lean.MessageData) (k : Lean.MetaM Unit) :
                  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
                              def Aesop.Rapp.traceMetadata.trc (traceOpt : TraceOption) (m : Lean.MessageData) :
                              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