class Data.DataString.IsString (α : Type u) : Type u

Overloaded string literals. A type α with an IsString instance can be constructed from a String literal.

$$\text{fromString} : \text{String} \to \alpha$$

• fromString : String → α

  Convert a String to the target type.

@[implicit_reducible]

instance Data.DataString.instIsStringString : IsString String

Equations

• Data.DataString.instIsStringString = { fromString := id }

def Data.DataString.lines (s : String) : List String

Split a string into lines (on '\n').

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

Equations

• Data.DataString.lines s = s.splitOn "\n"

def Data.DataString.words (s : String) : List String

Split a string into words (on whitespace).

$$\text{words}(\text{"hello world"}) = [\text{"hello"}, \text{"world"}]$$

Equations

• Data.DataString.words s = Data.DataString.words.go [] s.toList []

def Data.DataString.words.go (acc rest : List Char) (result : List String) : List String

Equations

• One or more equations did not get rendered due to their size.
• Data.DataString.words.go acc [] result = if acc.isEmpty = true then result.reverse else (String.ofList acc.reverse :: result).reverse

def Data.DataString.unlines (ls : List String) : String

Join lines with '\n'.

$$\text{unlines}([\text{"a"}, \text{"b"}]) = \text{"a\\nb\\n"}$$

Equations

• Data.DataString.unlines ls = "\n".intercalate ls ++ if ls.isEmpty = true then "" else "\n"

def Data.DataString.unwords (ws : List String) : String

Join words with ' '.

$$\text{unwords}([\text{"hello"}, \text{"world"}]) = \text{"hello world"}$$

Equations

• Data.DataString.unwords ws = " ".intercalate ws

theorem Data.DataString.unwords_nil : unwords [] = ""

unwords of empty list is empty.