Documentation

Aesop.Tracing

source
structure Aesop.TraceOption :
Type
Instances For
    source
    def Aesop.instInhabitedTraceOption.default :
    TraceOption
    Instances For
      source
      @[implicit_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