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
        • { data := d1 }.IsPrefix { data := d2 } = (d1 <+: d2)
        Instances For

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

          Equations
          • { data := d1 }.IsSuffix { 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

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

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