Documentation

Hale.Text.Data.Text

@[reducible, inline]
abbrev Data.Text :

Unicode text type. Lean's String is already UTF-8 encoded Unicode. $$\text{Text} := \text{String}$$

Equations
Instances For
    @[inline]

    Convert a list of characters to Text. $$\text{pack}([c_1, \ldots, c_n]) = \text{"c_1 \ldots c_n"}$$

    Equations
    Instances For
      @[inline]

      Convert Text to a list of characters. $$\text{unpack}(t) = [t_0, t_1, \ldots, t_{n-1}]$$

      Equations
      Instances For
        @[inline]

        A Text containing a single character. $$\text{singleton}(c) = \text{"c"}$$

        Equations
        Instances For
          @[inline]

          The empty Text. $$\text{empty} = \text{""}$$

          Equations
          Instances For
            @[inline]

            Is the Text empty? $$\text{null}(t) \iff |t| = 0$$

            Equations
            Instances For
              @[inline]

              The number of characters (code points) in the Text. $$\text{length}(t) = |t|$$

              Equations
              Instances For

                Compare the length of a Text against a Nat. Returns Ordering.lt, Ordering.eq, or Ordering.gt. $$\text{compareLength}(t, n) = \text{compare}(|t|, n)$$

                Equations
                Instances For
                  def Data.Text.map (f : CharChar) (t : Text) :

                  Apply a function to every character. $$\text{map}(f, t) = \text{pack}(\text{List.map}\ f\ (\text{unpack}\ t))$$

                  Equations
                  Instances For

                    Insert a separator Text between elements and concatenate. $$\text{intercalate}(sep, [t_1, \ldots, t_k]) = t_1 \mathbin{+\!\!+} sep \mathbin{+\!\!+} \cdots \mathbin{+\!\!+} t_k$$

                    Equations
                    Instances For

                      Insert a character between each character of the Text. $$\text{intersperse}(c, \text{"abc"}) = \text{"acbcc"}$$

                      Equations
                      Instances For

                        Transpose rows and columns of a list of Texts. $$\text{transpose}([\text{"ab"}, \text{"cd"}]) = [\text{"ac"}, \text{"bd"}]$$

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          Instances For

                            Reverse the characters. $$\text{reverse}(\text{"abc"}) = \text{"cba"}$$

                            Equations
                            Instances For
                              def Data.Text.replace (needle replacement t : Text) :

                              Replace all non-overlapping occurrences of needle with replacement. $$\text{replace}(\text{needle}, \text{replacement}, t)$$

                              Equations
                              Instances For

                                Case-fold: convert to lower case for case-insensitive comparisons. $$\text{toCaseFold}(t) \approx \text{toLower}(t)$$ Note: Full Unicode case folding is approximated by toLower.

                                Equations
                                Instances For

                                  Convert all characters to lower case. $$\text{toLower}(\text{"ABC"}) = \text{"abc"}$$

                                  Equations
                                  Instances For

                                    Convert all characters to upper case. $$\text{toUpper}(\text{"abc"}) = \text{"ABC"}$$

                                    Equations
                                    Instances For

                                      Title case: capitalize the first character, lowercase the rest. $$\text{toTitle}(\text{"hello world"}) = \text{"Hello world"}$$

                                      Equations
                                      Instances For
                                        def Data.Text.justifyLeft (n : Nat) (c : Char) (t : Text) :

                                        Left-justify to width n with fill character c. $$\text{justifyLeft}(n, c, t) = t \mathbin{+\!\!+} \text{replicate}(n - |t|, c)$$

                                        Equations
                                        Instances For
                                          def Data.Text.justifyRight (n : Nat) (c : Char) (t : Text) :

                                          Right-justify to width n with fill character c. $$\text{justifyRight}(n, c, t) = \text{replicate}(n - |t|, c) \mathbin{+\!\!+} t$$

                                          Equations
                                          Instances For
                                            def Data.Text.center (n : Nat) (c : Char) (t : Text) :

                                            Center-justify to width n with fill character c. $$\text{center}(n, c, t)$$ pads equally on both sides.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              def Data.Text.foldl {α : Type u_1} (f : αCharα) (z : α) (t : Text) :
                                              α

                                              Left fold over characters. $$\text{foldl}(f, z, t) = f(\ldots f(f(z, t_0), t_1) \ldots, t_{n-1})$$

                                              Equations
                                              Instances For
                                                @[inline]
                                                def Data.Text.foldl' {α : Type u_1} (f : αCharα) (z : α) (t : Text) :
                                                α

                                                Strict left fold (same as foldl in Lean since evaluation is strict). $$\text{foldl'}(f, z, t) = \text{foldl}(f, z, t)$$

                                                Equations
                                                Instances For
                                                  def Data.Text.foldr {α : Type u_1} (f : Charαα) (z : α) (t : Text) :
                                                  α

                                                  Right fold over characters. $$\text{foldr}(f, z, t) = f(t_0, f(t_1, \ldots f(t_{n-1}, z)))$$

                                                  Equations
                                                  Instances For

                                                    Concatenate a list of Texts. $$\text{concat}([t_1, \ldots, t_k]) = t_1 \mathbin{+\!\!+} \cdots \mathbin{+\!\!+} t_k$$

                                                    Equations
                                                    Instances For
                                                      def Data.Text.concatMap (f : CharText) (t : Text) :

                                                      Map a function over characters and concatenate the results. $$\text{concatMap}(f, t) = \text{concat}(\text{map}(f, \text{unpack}(t)))$$

                                                      Equations
                                                      Instances For
                                                        def Data.Text.any (p : CharBool) (t : Text) :

                                                        Does any character satisfy the predicate? $$\text{any}(p, t) = \exists c \in t.\; p(c)$$

                                                        Equations
                                                        Instances For
                                                          def Data.Text.all (p : CharBool) (t : Text) :

                                                          Do all characters satisfy the predicate? $$\text{all}(p, t) = \forall c \in t.\; p(c)$$

                                                          Equations
                                                          Instances For
                                                            def Data.Text.maximum (t : Text) (h : (String.toList t).length > 0 := by simp) :

                                                            Maximum character in a non-empty Text. $$\text{maximum}(t) = \max(t),\quad \text{requires } |t| > 0$$

                                                            Instances For
                                                              def Data.Text.minimum (t : Text) (h : (String.toList t).length > 0 := by simp) :

                                                              Minimum character in a non-empty Text. $$\text{minimum}(t) = \min(t),\quad \text{requires } |t| > 0$$

                                                              Instances For
                                                                def Data.Text.head (t : Text) (h : (String.toList t).length > 0 := by simp) :

                                                                The first character of a non-empty Text. $$\text{head}(t) = t_0,\quad \text{requires } |t| > 0$$

                                                                Instances For
                                                                  def Data.Text.last (t : Text) (h : (String.toList t).length > 0 := by simp) :

                                                                  The last character of a non-empty Text. $$\text{last}(t) = t_{|t|-1},\quad \text{requires } |t| > 0$$

                                                                  Instances For
                                                                    def Data.Text.tail (t : Text) (h : (String.toList t).length > 0 := by simp) :

                                                                    All characters except the first. $$\text{tail}(t) = t[1..],\quad \text{requires } |t| > 0$$

                                                                    Instances For
                                                                      def Data.Text.init (t : Text) (h : (String.toList t).length > 0 := by simp) :

                                                                      All characters except the last. $$\text{init}(t) = t[..|t|-1],\quad \text{requires } |t| > 0$$

                                                                      Equations
                                                                      Instances For
                                                                        @[inline]
                                                                        def Data.Text.cons (c : Char) (t : Text) :

                                                                        Prepend a character. $$\text{cons}(c, t) = c : t$$

                                                                        Equations
                                                                        Instances For
                                                                          @[inline]
                                                                          def Data.Text.snoc (t : Text) (c : Char) :

                                                                          Append a character. $$\text{snoc}(t, c) = t \mathbin{+\!\!+} [c]$$

                                                                          Equations
                                                                          Instances For
                                                                            @[inline]

                                                                            Append two Texts. $$\text{append}(s, t) = s \mathbin{+\!\!+} t$$

                                                                            Equations
                                                                            Instances For

                                                                              Decompose into head and tail, or none if empty. $$\text{uncons}(t) = \begin{cases} \text{some}(t_0, t[1..]) & |t| > 0 \\ \text{none} & |t| = 0 \end{cases}$$

                                                                              Equations
                                                                              Instances For

                                                                                Decompose into init and last, or none if empty. $$\text{unsnoc}(t) = \begin{cases} \text{some}(t[..|t|-1], t_{|t|-1}) & |t| > 0 \\ \text{none} & |t| = 0 \end{cases}$$

                                                                                Equations
                                                                                Instances For
                                                                                  def Data.Text.take (n : Nat) (t : Text) :

                                                                                  Take the first n characters. $$\text{take}(n, t) = t[0..n]$$

                                                                                  Equations
                                                                                  Instances For
                                                                                    def Data.Text.drop (n : Nat) (t : Text) :

                                                                                    Drop the first n characters. $$\text{drop}(n, t) = t[n..]$$

                                                                                    Equations
                                                                                    Instances For
                                                                                      def Data.Text.takeWhile (p : CharBool) (t : Text) :

                                                                                      Take characters from the front while the predicate holds. $$\text{takeWhile}(p, t) = t[0..k]$$ where $k$ is the first index where $p$ fails.

                                                                                      Equations
                                                                                      Instances For
                                                                                        def Data.Text.dropWhile (p : CharBool) (t : Text) :

                                                                                        Drop characters from the front while the predicate holds. $$\text{dropWhile}(p, t) = t[k..]$$ where $k$ is the first index where $p$ fails.

                                                                                        Equations
                                                                                        Instances For

                                                                                          Drop characters from the end while the predicate holds. $$\text{dropWhileEnd}(p, t)$$

                                                                                          Equations
                                                                                          Instances For
                                                                                            def Data.Text.dropAround (p : CharBool) (t : Text) :

                                                                                            Drop characters from both ends while the predicate holds. $$\text{dropAround}(p, t) = \text{dropWhile}(p, \text{dropWhileEnd}(p, t))$$

                                                                                            Equations
                                                                                            Instances For

                                                                                              Strip leading and trailing whitespace. $$\text{strip}(t)$$

                                                                                              Equations
                                                                                              Instances For

                                                                                                Strip leading whitespace. $$\text{stripStart}(t)$$

                                                                                                Equations
                                                                                                Instances For

                                                                                                  Strip trailing whitespace. $$\text{stripEnd}(t)$$

                                                                                                  Equations
                                                                                                  Instances For

                                                                                                    Split at position n. $$\text{splitAt}(n, t) = (\text{take}(n, t), \text{drop}(n, t))$$

                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      def Data.Text.breakOn (needle t : Text) :

                                                                                                      Break a Text at the first occurrence of needle. Returns (before, matchAndAfter). If not found, returns (t, ""). $$\text{breakOn}(\text{needle}, t) = (t[..i], t[i..])$$

                                                                                                      Equations
                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                      Instances For

                                                                                                        Break a Text at the last occurrence of needle. Returns (beforeAndMatch, after). If not found, returns ("", t). $$\text{breakOnEnd}(\text{needle}, t)$$

                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For
                                                                                                          def Data.Text.break_ (p : CharBool) (t : Text) :

                                                                                                          Break at the first character where the predicate holds. $$\text{break\_}(p, t) = (\text{takeWhile}(\neg p, t), \text{dropWhile}(\neg p, t))$$

                                                                                                          Equations
                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                          Instances For
                                                                                                            def Data.Text.span (p : CharBool) (t : Text) :

                                                                                                            Span: take while predicate holds, then return both parts. $$\text{span}(p, t) = (\text{takeWhile}(p, t), \text{dropWhile}(p, t))$$

                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              def Data.Text.groupBy (eq : CharCharBool) (t : Text) :

                                                                                                              Group consecutive characters by a custom equality. $$\text{groupBy}(eq, t)$$

                                                                                                              Equations
                                                                                                              Instances For

                                                                                                                Group consecutive equal characters. $$\text{group}(\text{"aabbbca"}) = [\text{"aa"}, \text{"bbb"}, \text{"c"}, \text{"a"}]$$

                                                                                                                Equations
                                                                                                                Instances For

                                                                                                                  All initial segments. $$\text{inits}(\text{"abc"}) = [\text{""}, \text{"a"}, \text{"ab"}, \text{"abc"}]$$

                                                                                                                  Equations
                                                                                                                  Instances For

                                                                                                                    All final segments. $$\text{tails}(\text{"abc"}) = [\text{"abc"}, \text{"bc"}, \text{"c"}, \text{""}]$$

                                                                                                                    Equations
                                                                                                                    Instances For

                                                                                                                      Split on a separator string. $$\text{splitOn}(\text{","}, \text{"a,b,c"}) = [\text{"a"}, \text{"b"}, \text{"c"}]$$

                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        def Data.Text.split (p : CharBool) (t : Text) :

                                                                                                                        Split on characters satisfying a predicate. $$\text{split}(p, t)$$ splits at every character where $p$ holds.

                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          Equations
                                                                                                                          Instances For

                                                                                                                            Split into chunks of at most n characters. Fuel-limited to ensure termination. $$\text{chunksOf}(n, t)$$

                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              Equations
                                                                                                                              Instances For

                                                                                                                                Split into lines. $$\text{lines}(\text{"a\\nb\\nc"}) = [\text{"a"}, \text{"b"}, \text{"c"}]$$

                                                                                                                                Equations
                                                                                                                                Instances For

                                                                                                                                  Split into words (on whitespace). $$\text{words}(\text{"hello world"}) = [\text{"hello"}, \text{"world"}]$$

                                                                                                                                  Equations
                                                                                                                                  Instances For

                                                                                                                                    Join lines with newlines. $$\text{unlines}([\text{"a"}, \text{"b"}]) = \text{"a\\nb\\n"}$$

                                                                                                                                    Equations
                                                                                                                                    Instances For

                                                                                                                                      Join words with spaces. $$\text{unwords}([\text{"hello"}, \text{"world"}]) = \text{"hello world"}$$

                                                                                                                                      Equations
                                                                                                                                      Instances For

                                                                                                                                        Is pfx a prefix of t? $$\text{isPrefixOf}(\text{pfx}, t) \iff t \text{ starts with } \text{pfx}$$

                                                                                                                                        Equations
                                                                                                                                        Instances For

                                                                                                                                          Is sfx a suffix of t? $$\text{isSuffixOf}(\text{sfx}, t) \iff t \text{ ends with } \text{sfx}$$

                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            def Data.Text.isInfixOf (needle t : Text) :

                                                                                                                                            Is needle contained in t? $$\text{isInfixOf}(\text{needle}, t) \iff \text{needle} \subseteq t$$

                                                                                                                                            Equations
                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                            Instances For
                                                                                                                                              Equations
                                                                                                                                              Instances For

                                                                                                                                                Strip a prefix, returning none if not a prefix. $$\text{stripPrefix}(\text{pfx}, t)$$

                                                                                                                                                Equations
                                                                                                                                                Instances For

                                                                                                                                                  Strip a suffix, returning none if not a suffix. $$\text{stripSuffix}(\text{sfx}, t)$$

                                                                                                                                                  Equations
                                                                                                                                                  Instances For
                                                                                                                                                    def Data.Text.elem (c : Char) (t : Text) :

                                                                                                                                                    Does the character occur in the Text? $$\text{elem}(c, t) = \exists i.\; t_i = c$$

                                                                                                                                                    Equations
                                                                                                                                                    Instances For
                                                                                                                                                      def Data.Text.find (p : CharBool) (t : Text) :

                                                                                                                                                      Find the first character satisfying a predicate. $$\text{find}(p, t)$$

                                                                                                                                                      Equations
                                                                                                                                                      Instances For
                                                                                                                                                        def Data.Text.filter (p : CharBool) (t : Text) :

                                                                                                                                                        Keep only characters satisfying a predicate. $$\text{filter}(p, t) = [c \in t \mid p(c)]$$

                                                                                                                                                        Equations
                                                                                                                                                        Instances For

                                                                                                                                                          Partition into (satisfying, not-satisfying). $$\text{partition}(p, t) = (\text{filter}(p, t), \text{filter}(\neg p, t))$$

                                                                                                                                                          Equations
                                                                                                                                                          Instances For

                                                                                                                                                            Index into the Text with a bounds check. $$\text{index}(t, i) = t_i$$

                                                                                                                                                            Equations
                                                                                                                                                            Instances For
                                                                                                                                                              def Data.Text.count (needle t : Text) :

                                                                                                                                                              Count non-overlapping occurrences of a substring. $$\text{count}(\text{needle}, t)$$

                                                                                                                                                              Equations
                                                                                                                                                              Instances For

                                                                                                                                                                Zip two Texts into a list of character pairs. $$\text{zip}(s, t) = [(s_0, t_0), (s_1, t_1), \ldots]$$

                                                                                                                                                                Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  def Data.Text.zipWith (f : CharCharChar) (s t : Text) :

                                                                                                                                                                  Zip two Texts with a combining function. $$\text{zipWith}(f, s, t) = [f(s_0, t_0), f(s_1, t_1), \ldots]$$

                                                                                                                                                                  Equations
                                                                                                                                                                  Instances For

                                                                                                                                                                    pack and unpack are inverses. $$\text{pack}(\text{unpack}(t)) = t$$

                                                                                                                                                                    theorem Data.Text.unpack_pack (cs : List Char) :
                                                                                                                                                                    (pack cs).unpack = cs

                                                                                                                                                                    unpack and pack are inverses. $$\text{unpack}(\text{pack}(cs)) = cs$$

                                                                                                                                                                    empty is null. $$\text{null}(\text{empty}) = \text{true}$$

                                                                                                                                                                    length of empty is zero. $$\text{length}(\text{empty}) = 0$$

                                                                                                                                                                    singleton produces a text of length 1. $$\text{length}(\text{singleton}(c)) = 1$$

                                                                                                                                                                    singleton is not null. $$\text{null}(\text{singleton}(c)) = \text{false}$$

                                                                                                                                                                    theorem Data.Text.length_cons (c : Char) (t : Text) :
                                                                                                                                                                    (cons c t).length = t.length + 1

                                                                                                                                                                    cons increases length by one. $$\text{length}(\text{cons}(c, t)) = \text{length}(t) + 1$$

                                                                                                                                                                    append with empty on the left is identity. $$\text{append}(\text{empty}, t) = t$$

                                                                                                                                                                    append with empty on the right is identity. $$\text{append}(t, \text{empty}) = t$$

                                                                                                                                                                    reverse of empty is empty. $$\text{reverse}(\text{empty}) = \text{empty}$$

                                                                                                                                                                    reverse is an involution. $$\text{reverse}(\text{reverse}(t)) = t$$