Documentation

Aesop.Tracing

source
structure Aesop.TraceOption :
Type
Instances For
    source
    @[instance_reducible]
    instance Aesop.instInhabitedTraceOption :
    Inhabited TraceOption
    source
    def Aesop.registerTraceOption (traceName : Lean.Name) (descr : String) :
    IO TraceOption
    Instances For
      source
      def Aesop.TraceOption.isEnabled {m : Type → Type} [Monad m] [Lean.MonadOptions m] (opt : TraceOption) :
      m Bool
      Instances For
        source
        def Aesop.TraceOption.withEnabled {m : Type → Type} {α : Type} [Lean.MonadWithOptions m] (opt : TraceOption) (k : m α) :
        m α
        Instances For
          source
          opaque Aesop.TraceOption.steps :
          TraceOption
          source
          opaque Aesop.TraceOption.ruleSet :
          TraceOption
          source
          opaque Aesop.TraceOption.proof :
          TraceOption
          source
          opaque Aesop.TraceOption.tree :
          TraceOption
          source
          opaque Aesop.TraceOption.extraction :
          TraceOption
          source
          opaque Aesop.TraceOption.stats :
          TraceOption
          source
          opaque Aesop.TraceOption.debug :
          TraceOption
          source
          opaque Aesop.TraceOption.script :
          TraceOption
          source
          opaque Aesop.TraceOption.forward :
          TraceOption
          source
          opaque Aesop.TraceOption.forwardDebug :
          TraceOption
          source
          opaque Aesop.TraceOption.rpinf :
          TraceOption
          source
          def Aesop.resolveTraceOption (stx : Lean.Ident) :
          Lean.MacroM Lean.Name
          Instances For
            source
            def Aesop.«doElemAesop_trace![_]__» :
            Lean.ParserDescr
            Instances For
              source
              def Aesop.«doElemAesop_trace[_]__» :
              Lean.ParserDescr
              Instances For
                source
                def Aesop.ruleSuccessEmoji :
                String
                Instances For
                  source
                  def Aesop.ruleFailureEmoji :
                  String
                  Instances For
                    source
                    def Aesop.ruleProvedEmoji :
                    String
                    Instances For
                      source
                      def Aesop.ruleErrorEmoji :
                      String
                      Instances For
                        source
                        def Aesop.rulePostponedEmoji :
                        String
                        Instances For
                          source
                          def Aesop.ruleSkippedEmoji :
                          String
                          Instances For
                            source
                            def Aesop.nodeUnknownEmoji :
                            String
                            Instances For
                              source
                              def Aesop.nodeProvedEmoji :
                              String
                              Instances For
                                source
                                def Aesop.nodeUnprovableEmoji :
                                String
                                Instances For
                                  source
                                  def Aesop.newNodeEmoji :
                                  String
                                  Instances For
                                    source
                                    def Aesop.exceptRuleResultToEmoji {α : Type u_1} {ε : Type u_2} (toEmoji : α → String) :
                                    Except ε α → String
                                    Instances For
                                      source
                                      @[always_inline]
                                      def Aesop.withAesopTraceNode {m : Type → Type} {ε : Type} [Monad m] [Lean.MonadTrace m] [MonadLiftT BaseIO m] [Lean.MonadRef m] [Lean.AddMessageContext m] [Lean.MonadOptions m] [Lean.MonadAlwaysExcept ε m] {α : Type} [Lean.ExceptToTraceResult ε α] (opt : TraceOption) (msg : Except ε α → m Lean.MessageData) (k : m α) (collapsed : Bool := true) :
                                      m α
                                      Instances For
                                        source
                                        @[always_inline]
                                        def Aesop.withAesopTraceNodeBefore {m : Type → Type} {ε : Type} [Monad m] [Lean.MonadTrace m] [MonadLiftT BaseIO m] [Lean.MonadRef m] [Lean.AddMessageContext m] [Lean.MonadOptions m] [Lean.MonadAlwaysExcept ε m] {α : Type} [Lean.ExceptToTraceResult ε α] (opt : TraceOption) (msg : m Lean.MessageData) (k : m α) (collapsed : Bool := true) :
                                        m α
                                        Instances For
                                          source
                                          @[always_inline]
                                          def Aesop.withConstAesopTraceNode {m : Type → Type} {ε : Type} [Monad m] [Lean.MonadTrace m] [MonadLiftT BaseIO m] [Lean.MonadRef m] [Lean.AddMessageContext m] [Lean.MonadOptions m] [Lean.MonadAlwaysExcept ε m] {α : Type} [Lean.ExceptToTraceResult ε α] (opt : TraceOption) (msg : m Lean.MessageData) (k : m α) (collapsed : Bool := true) :
                                          m α
                                          Instances For
                                            source
                                            def Aesop.traceSimpTheoremTreeContents (t : Lean.Meta.SimpTheoremTree) (opt : TraceOption) :
                                            Lean.CoreM Unit
                                            Instances For
                                              source
                                              def Aesop.traceSimpTheorems (s : Lean.Meta.SimpTheorems) (opt : TraceOption) :
                                              Lean.CoreM Unit
                                              Instances For