Documentation

Lean.Meta.Tactic.Simp.BuiltinSimprocs.String

source
def String.reduceAppend :
Lean.Meta.Simp.DSimproc
Instances For
    source
    def String.reduceOfList :
    Lean.Meta.Simp.DSimproc
    Instances For
      source
      def String.reduceToList :
      Lean.Meta.Simp.DSimproc
      Instances For
        source
        def String.reducePush :
        Lean.Meta.Simp.DSimproc
        Instances For
          source
          def String.reduceSingleton :
          Lean.Meta.Simp.DSimproc
          Instances For
            source
            def String.reduceToSingleton :
            Lean.Meta.Simp.DSimproc
            Instances For
              source
              def String.reduceLT :
              Lean.Meta.Simp.Simproc
              Instances For
                source
                def String.reduceLE :
                Lean.Meta.Simp.Simproc
                Instances For
                  source
                  def String.reduceGT :
                  Lean.Meta.Simp.Simproc
                  Instances For
                    source
                    def String.reduceGE :
                    Lean.Meta.Simp.Simproc
                    Instances For
                      source
                      def String.reduceEq :
                      Lean.Meta.Simp.Simproc
                      Instances For
                        source
                        def String.reduceNe :
                        Lean.Meta.Simp.Simproc
                        Instances For
                          source
                          def String.reduceBEq :
                          Lean.Meta.Simp.DSimproc
                          Instances For
                            source
                            def String.reduceBNe :
                            Lean.Meta.Simp.DSimproc
                            Instances For