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

      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

            getRest s t returns some r if s = t ++ r. If t is not a prefix of s, it returns none.

            Equations
            Instances For

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

              Equations
              Instances For