string

Pos.equal

def Pos.equal (p : Pos) (q : Pos) : Bool

Whether two binary positive numbers are equal, compared bit by bit.

Bin.equal

def Bin.equal (a : Bin) (b : Bin) : Bool

Whether two binary natural numbers are equal.

Pos.toNat

def Pos.toNat (p : Pos) : Nat

A binary positive number as a natural number.

Pos.ofNat

def Pos.ofNat (bits : Nat) (n : Nat) : Pos

A positive natural number in binary, the least significant bit outermost; bits bounds the number of bits.

Char.code

def code (c : Char) : Nat

The code point of a character.

Char.ofCode

def ofCode (n : Nat) : Char

The character of a code point (64 bits are enough for any code point).

Char.equal

def equal (c : Char) (d : Char) : Bool

Whether two characters are the same code point.

Char.ofDigit

def ofDigit (d : Nat) : Char

The digit character of a number from 0 to 9.

Char.positionIn

def positionIn (c : Char) (cs : List Char) (i : Nat) : Option Nat

The position of a character in a list, counting from i.

Char.digit

def digit (c : Char) : Option Nat

The value of a decimal digit character, or none for any other character.

Char.inRange

def inRange (low : Nat) (high : Nat) (c : Char) : Bool

Whether a character’s code point is from low to high.

Char.isDigit

def isDigit (c : Char) : Bool

Whether a character is an ASCII decimal digit.

Char.isUpper

def isUpper (c : Char) : Bool

Whether a character is an ASCII uppercase letter.

Char.isLower

def isLower (c : Char) : Bool

Whether a character is an ASCII lowercase letter.

Char.isAlpha

def isAlpha (c : Char) : Bool

Whether a character is an ASCII letter.

Char.isAlphanumeric

def isAlphanumeric (c : Char) : Bool

Whether a character is an ASCII letter or digit.

Char.isSpace

def isSpace (c : Char) : Bool

Whether a character is whitespace: a space, a tab, a carriage return or a newline.

Char.toUpper

def toUpper (c : Char) : Char

An ASCII lowercase letter in uppercase; any other character as it is.

Char.toLower

def toLower (c : Char) : Char

An ASCII uppercase letter in lowercase; any other character as it is.

Nat.hexDigit

def Nat.hexDigit (d : Nat) : Char

The lowercase hexadecimal digit of a number from 0 to 15.

Decimal.lastDigit

def lastDigit (n : Nat) : Char

The last decimal digit of a number, as a character.

Decimal.digits

def digits (fuel : Nat) (n : Nat) (rest : List Char) : List Char

The decimal digits of n in front of rest, by repeated division by 10; fuel only bounds the recursion (it stops when n < 10).

Decimal.read

def read (cs : List Char) (read : Nat) : Option Nat

The number decimal digits give, read onto read; none at a character that is not a digit.

Nat.decimal

def Nat.decimal (n : Nat) : String

The decimal digits of a natural number (toString n is the same).

String.chars

def chars (s : String) : List Char

The characters of a string.

String.append

def append (a : String) (b : String) : String

Two strings one after the other.

String.length

def length (s : String) : Nat

The number of characters of a string (not of bytes).

String.sameChars

def sameChars (cs : List Char) (ds : List Char) : Bool

Whether two lists of characters are the same, character by character.

String.equal

def equal (a : String) (b : String) : Bool

Whether two strings have the same characters.

String.concat

def concat (xs : List String) : String

The strings of a list one after the other; f"..." expands to it.

String.charsAfter

def charsAfter (start : List Char) (cs : List Char) : Option (List Char)

The characters after a prefix, if the characters start with it.

String.cutAt

def cutAt (sep : List Char) (fuel : Nat) (cs : List Char) (piece : List Char) : List (List Char)

Characters cut at every occurrence of a separator (not empty), the piece so far in reverse; fuel bounds the recursion.

String.split

def split (s : String) (sep : String) : List String

A string cut at every occurrence of a separator, left to right; an empty separator gives the whole string.

String.join

def join (sep : String) (xs : List String) : String

The strings of a list with a separator between each two.

String.isEmpty

def isEmpty (s : String) : Bool

Whether a string has no characters.

String.lines

def lines (s : String) : List String

The lines of a string, cut at each newline.

String.words

def words (s : String) : List String

The words of a string: the pieces between spaces that are not empty.

String.toNat

def toNat (s : String) : Option Nat

The number a non-empty string of decimal digits writes, or none.

String.startsWith

def startsWith (s : String) (start : String) : Bool

Whether a string starts with a prefix.

String.reversed

def reversed (s : String) : String

A string’s characters in reverse order.

String.endsWith

def endsWith (s : String) (ending : String) : Bool

Whether a string ends with a suffix.

String.take

def take (n : Nat) (s : String) : String

The first n characters of a string.

String.drop

def drop (n : Nat) (s : String) : String

A string without its first n characters.

String.dropSpaces

def dropSpaces (cs : List Char) : List Char

Characters without the whitespace at their start.

String.trim

def trim (s : String) : String

A string without the whitespace at its start and end.

String.positionIn

def positionIn (part : List Char) (cs : List Char) (i : Nat) : Option Nat

The position of the first occurrence of a part in characters, counting from i.

String.indexOf

def indexOf (s : String) (part : String) : Option Nat

The character position of the first occurrence of a part in a string, if it occurs.

String.contains

def contains (s : String) (part : String) : Bool

Whether a part occurs in a string.

String.replacedIn

def replacedIn (part : List Char) (replacement : List Char) (fuel : Nat) (cs : List Char) : List Char

Characters with every occurrence of a part (not empty) replaced, left to right; fuel bounds the recursion.

String.replace

def replace (s : String) (part : String) (replacement : String) : String

A string with every occurrence of a part replaced, left to right and not overlapping; an empty part changes nothing.

String.toUpper

def toUpper (s : String) : String

A string with its ASCII letters in uppercase.

String.toLower

def toLower (s : String) : String

A string with its ASCII letters in lowercase.

String.repeat

def repeat (n : Nat) (s : String) : String

A string n times.

String.padding

def padding (n : Nat) (pad : String) : List Char

The first n characters of a padding repeated.

String.padStart

def padStart (n : Nat) (pad : String) (s : String) : String

A string padded at its start up to n characters (a longer one as it is).

String.padEnd

def padEnd (n : Nat) (pad : String) (s : String) : String

A string padded at its end up to n characters (a longer one as it is).

String.nonEmptyLines

def nonEmptyLines (s : String) : List String

The lines of a string that are not empty after trimming, trimmed.

ToString

class ToString (A : Type)

Types whose values can be shown as a string.

toStringNat

instance toStringNat : ToString Nat

A natural number in decimal.

toStringBool

instance toStringBool : ToString Bool

true and false.

toStringString

instance toStringString : ToString String

A string as itself.

toStringList

instance toStringList {A : Type} {{d : ToString A}} : ToString (List A)

A list as [a, b, c].

toStringOption

instance toStringOption {A : Type} {{d : ToString A}} : ToString (Option A)

An option as none or some a.

Decimal.hasDigits

def hasDigits (cs : List Char) : Bool

Whether there is at least one digit.

Decimal.bltAddLeft

def bltAddLeft (x : Nat) (n : Nat) (k : Nat) (h : Nat.blt x n = true) : Nat.blt x (add k n) = true

bltSuccR k times: x < n implies x < k + n.

Decimal.bltOfAddLeft

def bltOfAddLeft (m : Nat) (n : Nat) (k : Nat) (h : Nat.blt (add k m) n = true) : Nat.blt m n = true

bltPredL k times: k + m < n implies m < n.

Decimal.timesTenPlus

def timesTenPlus (d : Nat) (r : Nat) : Nat

d * 10 + r.

Decimal.shifted

def shifted (v : Nat) (n : Nat) : Nat

A value with the last digit of n appended: v * 10 + n mod 10.

Decimal.belowTimesTen

def belowTimesTen (d : Nat) (r : Nat) : Nat.blt d (succ (Decimal.timesTenPlus d r)) = true

d < d * 10 + r + 1.

Decimal.quotientBelow

def quotientBelow (D : Nat) (R : Nat) (k : Nat) (h : Nat.blt (Decimal.timesTenPlus D R) (succ k) = true) (hr : Nat.blt R 10 = true) (e : Nat.blt (Decimal.timesTenPlus D R) 10 = false) : Nat.blt D k = true

The next digit has fuel: from D * 10 + R < k + 1, R < 10 and D * 10 + R not below 10, D < k.

Decimal.quotientHasFuel

def quotientHasFuel (n : Nat) (k : Nat) (h : Nat.blt n (succ k) = true) (e : Nat.blt n 10 = false) : Nat.blt (Nat.div n 10) k = true

Dropping the last decimal digit of n (at least 10) leaves fuel: n < k + 1 implies n / 10 < k.

Decimal.digitOfDigit

def digitOfDigit (d : Nat) (h : Nat.blt d 10 = true) : Char.digit (Char.ofDigit d) = some d

Reading back one digit: the digit of Char.ofDigit d is d, for d < 10.

Decimal.value

def value (fuel : Nat) (read : Nat) (n : Nat) : Nat

The value read back from Decimal.digits, with the same fuel and recursion, onto read.

Decimal.digitsAfter

def digitsAfter (small : Bool) (fewer : Nat) (n : Nat) (rest : List Char) : List Char

Decimal.digits after its comparison with 10.

Decimal.valueAfter

def valueAfter (small : Bool) (fewer : Nat) (read : Nat) (n : Nat) : Nat

Decimal.value after its comparison with 10.

Decimal.readDigit

def readDigit (m : Option Nat) (rest : List Char) (read : Nat) : Option Nat

Decimal.read of a looked-up digit.

Decimal.readOne

def readOne (d : Nat) (h : Nat.blt d 10 = true) (rest : List Char) (read : Nat) : Decimal.read (cons (Char.ofDigit d) rest) read = Decimal.read rest (add (mul read 10) d)

Reading a digit d < 10 multiplies the value by ten and adds d.

Decimal.ReadsAfter

def ReadsAfter (small : Bool) (fewer : Nat) (n : Nat) (rest : List Char) (read : Nat) : Type

The statement of Decimal.readDigits after the comparison with 10.

Decimal.readDigits

def readDigits (fuel : Nat) : (n : Nat) -> (rest : List Char) -> (read : Nat) -> Decimal.read (Decimal.digits fuel n rest) read = Decimal.read rest (Decimal.value fuel read n)

Reading what Decimal.digits writes is reading on with the value of n, for any fuel.

Decimal.ValueAfter

def ValueAfter (small : Bool) (fewer : Nat) (n : Nat) : Type

The statement of Decimal.valueOfDigits after the comparison with 10.

Decimal.valueOfDigits

def valueOfDigits (fuel : Nat) : (n : Nat) -> Nat.blt n fuel = true -> Decimal.value fuel 0 n = n

With enough fuel (n < fuel), the value read back is n.

Decimal.digitsNotEmpty

def digitsNotEmpty (fuel : Nat) : (n : Nat) -> (c : Char) -> (rest : List Char) -> Decimal.hasDigits (Decimal.digits fuel n (cons c rest)) = true

Decimal.digits onto a non-empty list is not empty.

Decimal.decimalNotEmpty

def decimalNotEmpty (n : Nat) : Decimal.hasDigits (Decimal.digits (succ n) n nil) = true

The decimal digits of a number are not empty.

Decimal.toNatOf

def toNatOf (cs : List Char) : Option Nat

String.toNat of characters.

Decimal.toNatOfNotEmpty

def toNatOfNotEmpty (cs : List Char) (h : Decimal.hasDigits cs = true) : Decimal.toNatOf cs = Decimal.read cs 0

On characters that are not empty, String.toNat reads them.

String.toNatDecimal

def String.toNatDecimal (n : Nat) : String.toNat (Nat.decimal n) = some n

Reading back the decimal digits gives the number.