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 : optParam 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 : optParam 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
        • x✝.IsPrefix x = match x✝, x with | { data := d1 }, { data := d2 } => d1 <+: d2
        Instances For

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

          Equations
          • x✝.IsSuffix x = match x✝, x with | { data := d1 }, { data := d2 } => d1 <:+ d2
          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
              @[deprecated String.dropPrefix?]

              Alias of String.dropPrefix?.


              If pre is a prefix of s, i.e. s = pre ++ t, returns the remainder t.

              Equations
              Instances For

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

                Equations
                • s.head = s.iter.curr
                Instances For