Documentation

Mathlib.Data.String.Defs

Definitions for String #

This file defines a bunch of functions for the String datatype.

def String.leftpad (n : Nat) (c : Char := ' ') (s : String) :

Pad s : String with repeated occurrences of c : Char until it's of length n. If s is initially larger than n, just return s.

Equations
    Instances For
      def String.replicate (n : Nat) (c : Char) :

      Construct the string consisting of n copies of the character c.

      Equations
        Instances For
          def String.rightpad (n : Nat) (c : Char := ' ') (s : String) :

          Pad s : String with repeated occurrences of c : Char on the right until it's of length n. If s is initially larger than n, just return s.

          Equations
            Instances For

              s.IsPrefix t checks if the string s is a prefix of the string t.

              Equations
                Instances For

                  s.IsSuffix t checks if the string s is a suffix of the string t.

                  Equations
                    Instances For
                      def String.mapTokens (c : Char) (f : StringString) :

                      String.mapTokens c f s tokenizes s : string on c : char, maps f over each token, and then reassembles the string by intercalating the separator token c over the mapped tokens.

                      Equations
                        Instances For

                          Produce the head character from the string s, if s is not empty, otherwise 'A'.

                          Equations
                            Instances For