prelude

The basic types and what is done with them: Nat, Empty, pairs, Maybe, Either, Bytes (bytes has its operations); Bool, Unit and lists (builtin has them), lists’ :: and ++ (their other operations are List’s); numbers and strings, by the primitives, with their operators.

Nat

data Nat = Zero | Succ Nat

The natural numbers.

Empty

data Empty

Pair

data Pair a b = MkPair a b

Maybe

data Maybe a = Nothing | Just a

Either

data Either a b = Left a | Right b

Bytes

data Bytes

Bytes, not changed once made: a type of its own beside String, written b[...], whose operations are bytes’s (import bytes as Bytes), but its equality, instanceEqualityBytes, its Debug, instanceDebugBytes, and its Show, instanceShowBytes

Bits

data Bits

Bits, a bitstring of any length, not changed once made: a type of its own beside Bytes (which are whole bytes), written b[...] where its segments are not whole bytes (b[5::3]), whose operations are bits’s (import bits as Bits), but its equality, instanceEqualityBits, its Debug, instanceDebugBits, and its Show, instanceShowBits

::

(::) : {a : Type} -> a -> List a -> List a

x :: xs is Cons x xs; a pattern too, as it only names the tag

id

id : {a : Type} -> a -> a

const

const : {a b : Type} -> a -> b -> a

flip

flip : {a b c : Type} -> (a -> b -> c) -> b -> a -> c

compose

compose : {a b c : Type} -> (b -> c) -> (a -> b) -> a -> c

$

($) : {a b : Type} -> (a -> b) -> a -> b

Application, loosest: f $ g $ x is f (g x).

not

not : Bool -> Bool

&&

(&&) : Bool -> Bool -> Bool

||

(||) : Bool -> Bool -> Bool

Ordering

data Ordering = LT | EQ | GT

How one value is to another: less, equal, or greater.

Equality

theory Equality a where
  equal : a -> a -> Bool

A type’s equality: a function that compares values of a type it does not know asks for it, {{eq : Equality a}}, and is given the instance in scope of the type it is used at — the prelude’s of Int, Float64, String, Rune, Bool, Unit and Ordering, and of a List, a Maybe, a Pair and an Either of types that have one, found by finding theirs; a fixed-width type’s module’s of its own.

==

(==) : {a : Type} -> {{eq : Equality a}} -> a -> a -> Bool

/=

(/=) : {a : Type} -> {{eq : Equality a}} -> a -> a -> Bool

Order

theory Order a where
  eq : Equality a
  compare : a -> a -> Ordering
  lt : a -> a -> Bool
  le : a -> a -> Bool

A type’s order: its equality (eq), how two values are (compare), and whether one is less than the other, or not greater (lt, le: what < and <= are, as fast as the type has them) — the prelude’s of Int, Float64, String, Rune, Bool, Unit and Ordering, and of a List, a Maybe and a Pair of types that have one; a fixed-width type’s module’s of its own.

compare

compare : {a : Type} -> {{ord : Order a}} -> a -> a -> Ordering

<

(<) : {a : Type} -> {{ord : Order a}} -> a -> a -> Bool

<=

(<=) : {a : Type} -> {{ord : Order a}} -> a -> a -> Bool

>

(>) : {a : Type} -> {{ord : Order a}} -> a -> a -> Bool

>=

(>=) : {a : Type} -> {{ord : Order a}} -> a -> a -> Bool

min

min : {a : Type} -> {{ord : Order a}} -> a -> a -> a

The lesser of the two (the first, of two as great).

max

max : {a : Type} -> {{ord : Order a}} -> a -> a -> a

The greater of the two (the second, of two as great).

Addition

theory Addition a where
  add : a -> a -> a

+

(+) : {a : Type} -> {{add : Addition a}} -> a -> a -> a

Subtraction

theory Subtraction a where
  sub : a -> a -> a

-

(-) : {a : Type} -> {{sub : Subtraction a}} -> a -> a -> a

Multiplication

theory Multiplication a where
  mul : a -> a -> a

*

(*) : {a : Type} -> {{mul : Multiplication a}} -> a -> a -> a

Division

theory Division a where
  div : a -> a -> a

A type’s division, total: by zero, zero, as Lean’s and Coq’s are — no division abandons, and x / 0 is 0 (exception’s divOrThrow throws instead). Not a float’s: /. is a float’s, IEEE’s.

/

(/) : {a : Type} -> {{div : Division a}} -> a -> a -> a

Remainder

theory Remainder a where
  mod : a -> a -> a

The remainder of a type’s division, total: by zero, the dividend, so that (x / y) * y + x % y is x whatever y is.

%

(%) : {a : Type} -> {{mod : Remainder a}} -> a -> a -> a

Negation

theory Negation a where
  neg : a -> a

A type’s negation: what -x is, the neg in scope applied to x.

neg

neg : {a : Type} -> {{n : Negation a}} -> a -> a

FloatDivision

theory FloatDivision a where
  divide : a -> a -> a

A float type’s division, IEEE’s: by 0, an infinity (or not a number, of 0 by 0) — what /. is, the prelude’s of Float64, float32’s of Float32. An integer type has none: its division is /, total.

/.

(/.) : {a : Type} -> {{divide : FloatDivision a}} -> a -> a -> a

IsZero

theory IsZero a where
  isZero : a -> Bool

Whether a value is its type’s zero: what exception’s divOrThrow and modOrThrow ask of the divisor — the prelude’s of Int, a fixed-width integer type’s module’s of its own.

Bitwise

theory Bitwise a where
  and : a -> a -> a
  or : a -> a -> a
  xor : a -> a -> a
  complement : a -> a
  shiftL : a -> a -> a
  shiftR : a -> a -> a

An integer type’s bits, as two’s complement has them: the and, or and xor of two, every bit flipped, and shifts — an Int’s in int’s module, a fixed-width type’s in its own.

and

and : {a : Type} -> {{bits : Bitwise a}} -> a -> a -> a

The bits set in both.

or

or : {a : Type} -> {{bits : Bitwise a}} -> a -> a -> a

The bits set in either.

xor

xor : {a : Type} -> {{bits : Bitwise a}} -> a -> a -> a

The bits set in one of the two.

complement

complement : {a : Type} -> {{bits : Bitwise a}} -> a -> a

Every bit flipped.

shiftL

shiftL : {a : Type} -> {{bits : Bitwise a}} -> a -> a -> a

Shifted left by the second, as the type shifts.

shiftR

shiftR : {a : Type} -> {{bits : Bitwise a}} -> a -> a -> a

Shifted right by the second, as the type shifts.

intAdd

intAdd : Int -> Int -> Int

intSub

intSub : Int -> Int -> Int

intMul

intMul : Int -> Int -> Int

intDiv

intDiv : Int -> Int -> Int

intMod

intMod : Int -> Int -> Int

intEq

intEq : Int -> Int -> Bool

intLt

intLt : Int -> Int -> Bool

intLe

intLe : Int -> Int -> Bool

intShow

intShow : Int -> String

instanceEqualityInt

instance instanceEqualityInt : Equality Int

compareInt

compareInt : Int -> Int -> Ordering

instanceOrderInt

instance instanceOrderInt : Order Int

>>> 1 < 2 && 2 <= 2 || False
True
>>> ([max 2 (-3), min 2 (-3)] : List Int)
Cons 2 (Cons (-3) Nil)

instanceAdditionInt

instance instanceAdditionInt : Addition Int

instanceSubtractionInt

instance instanceSubtractionInt : Subtraction Int

instanceMultiplicationInt

instance instanceMultiplicationInt : Multiplication Int

instanceDivisionInt

instance instanceDivisionInt : Division Int

Division rounding down; by 0, 0.

instanceRemainderInt

instance instanceRemainderInt : Remainder Int

The remainder of /, of the sign of the divisor; by 0, the dividend.

>>> 1 + 2 * 3 - 4 / 2
5
>>> ([7 / 2, -7 / 2, 7 % 2, -7 % 2, 7 % -2] : List Int)
Cons 3 (Cons (-4) (Cons 1 (Cons 1 (Cons (-1) Nil))))
>>> ([7 / 0, 7 % 0, (7 / 0) * 0 + 7 % 0] : List Int)
Cons 0 (Cons 7 (Cons 7 Nil))

instanceNegationInt

instance instanceNegationInt : Negation Int

The integer of the other sign, 0 - x: what -x is.

>>> ([neg 5, -(3 - 10)] : List Int)
Cons (-5) (Cons 7 Nil)

instanceIsZeroInt

instance instanceIsZeroInt : IsZero Int

>>> ([instanceIsZeroInt.isZero 0, instanceIsZeroInt.isZero (-3)] : List Bool)
Cons True (Cons False Nil)

floatAdd

floatAdd : Float64 -> Float64 -> Float64

floatSub

floatSub : Float64 -> Float64 -> Float64

floatMul

floatMul : Float64 -> Float64 -> Float64

floatDiv

floatDiv : Float64 -> Float64 -> Float64

floatEq

floatEq : Float64 -> Float64 -> Bool

floatLt

floatLt : Float64 -> Float64 -> Bool

floatLe

floatLe : Float64 -> Float64 -> Bool

floatShow

floatShow : Float64 -> String

floatFromInt

floatFromInt : Int -> Float64

floatSqrt

floatSqrt : Float64 -> Float64

floatFloor

floatFloor : Float64 -> Int

instanceEqualityFloat64

instance instanceEqualityFloat64 : Equality Float64

compareFloat

compareFloat : Float64 -> Float64 -> Ordering

instanceOrderFloat64

instance instanceOrderFloat64 : Order Float64

instanceAdditionFloat64

instance instanceAdditionFloat64 : Addition Float64

instanceSubtractionFloat64

instance instanceSubtractionFloat64 : Subtraction Float64

instanceMultiplicationFloat64

instance instanceMultiplicationFloat64 : Multiplication Float64

instanceNegationFloat64

instance instanceNegationFloat64 : Negation Float64

The float of the other sign, 0.0’s too: what -x is.

instanceFloatDivisionFloat64

instance instanceFloatDivisionFloat64 : FloatDivision Float64

Division; by 0, an infinity (or not a number, of 0 by 0): a float has no /, whose division by 0 is 0.

>>> ([neg 2.5, -(1.0 - 3.5), 1.0 /. neg 0.0, 2.5 * 2.0 + 1.0] : List Float64)
[-2.5, 2.5, -Infinity, 6.0]

abs

abs : {a : Type} -> {{ord : Order a}} -> {{n : Negation a}} -> a -> a

x without its sign: the greater of x and -x.

>>> abs (-3)
3
>>> abs 7
7
>>> abs (-2.5)
2.5

toFloat

toFloat : Int -> Float64

floor

floor : Float64 -> Int

The greatest integer not above; of an infinity, or what is not a number, 0.

>>> ([floor 2.5, floor (-2.5), floor (1.0 /. 0.0), floor (-1.0 /. 0.0), floor (0.0 /. 0.0)] : List Int)
Cons 2 (Cons (-3) (Cons 0 (Cons 0 (Cons 0 Nil))))

sqrt

sqrt : Float64 -> Float64

strAppend

strAppend : String -> String -> String

strLength

strLength : String -> Int

strSlice

strSlice : String -> Int -> Int -> String

strEq

strEq : String -> String -> Bool

strLt

strLt : String -> String -> Bool

strCompare

strCompare : String -> String -> Int

strFind

strFind : String -> String -> Int -> Int

^

(^) : String -> String -> String

a ^ b: the string a, then b.

>>> "count: " ^ intShow (7 % 3)
"count: 1"
>>> "he" ^ "ff" ^ "!"
"heff!"

instanceEqualityString

instance instanceEqualityString : Equality String

bytesEq

bytesEq : Bytes -> Bytes -> Bool

bytesLength

bytesLength : Bytes -> Int

bytesSlice

bytesSlice : Bytes -> Int -> Int -> Bytes

bytesConcat

bytesConcat : List Bytes -> Bytes

bytesIntAt

bytesIntAt : Bytes -> Int -> Int -> Int -> Int

bytesOfInt

bytesOfInt : Int -> Int -> Int -> Bytes

bytesHasAt

bytesHasAt : Bytes -> Int -> Bytes -> Bool

bytesSized

bytesSized : Int -> Bytes -> Bytes

The first n bytes of b, as a segment x::binary-size(n) of a binary writes them: of fewer, abandoned.

instanceEqualityBytes

instance instanceEqualityBytes : Equality Bytes

Bytes’ (their other operations are bytes’s): the same bytes.

>>> b["hi", 255] == b[104, "i", 0xFF]
True

instanceEqualityRune

instance instanceEqualityRune : Equality Rune

instanceEqualityBool

instance instanceEqualityBool : Equality Bool

instanceEqualityUnit

instance instanceEqualityUnit : Equality Unit

instanceEqualityOrdering

instance instanceEqualityOrdering : Equality Ordering

equal

equal : {a : Type} -> {{eq : Equality a}} -> a -> a -> Bool

Whether the two are equal, as the instance of their type says.

>>> equal 3 3
True
>>> equal "heff" "help"
False
>>> equal 0.5 0.5 && not (equal 'a' 'b') && equal (1 < 2) True
True
>>> equal (compareInt 1 2) LT
True

instanceEqualityList

instance instanceEqualityList : {a : Type}
                              -> {{eq : Equality a}}
                              -> Equality (List a)

Lists are equal where they are as long, and equal element by element.

>>> equal ([1, 2] : List Int) [1, 2]
True
>>> equal ([[1, 2], [3]] : List (List Int)) [[1, 2], []]
False

instanceEqualityMaybe

instance instanceEqualityMaybe : {a : Type}
                               -> {{eq : Equality a}}
                               -> Equality (Maybe a)

>>> equal (Just 'h' : Maybe Rune) (Just 'h')
True
>>> equal (Just [1] : Maybe (List Int)) Nothing
False

instanceEqualityPair

instance instanceEqualityPair : {a b : Type}
                              -> {{eqA : Equality a}}
                              -> {{eqB : Equality b}}
                              -> Equality (a, b)

>>> equal (MkPair 1 "one" : Pair Int String) (MkPair 1 "one")
True

instanceEqualityEither

instance instanceEqualityEither : {a b : Type}
                                -> {{eqA : Equality a}}
                                -> {{eqB : Equality b}}
                                -> Equality (Either a b)

>>> equal (Left 1 : Either Int String) (Right "1")
False

fst

fst : {a b : Type} -> (a, b) -> a

snd

snd : {a b : Type} -> (a, b) -> b

maybe

maybe : {a b : Type} -> b -> (a -> b) -> Maybe a -> b

fromMaybe

fromMaybe : {a : Type} -> a -> Maybe a -> a

>>> fromMaybe 0 (Just 4)
4

either

either : {a b c : Type} -> (a -> c) -> (b -> c) -> Either a b -> c

Monad

theory Monad (m : Type -> Type) where
  pure : {a : Type} -> a -> m a
  bind : {a b : Type} -> m a -> (a -> m b) -> m b

A monad, no laws asked: a value as a computation (pure), and a computation and what comes after it as one (bind). do is not this: it takes the bind in scope by name, so a monad’s module keeps its own bind and pure, and builds its instance of them — the prelude’s of Maybe and Either e, co’s of Co h, generator’s of Generator. What is written once for every monad asks for one, {{mo : Monad m}}, and a module using it at its own monad gives its instance once: traverseS = traverse (mo := instanceMonadS).

>>=

(>>=) : {m : Type -> Type}
      -> {{mo : Monad m}}
      -> {a b : Type}
      -> m a
      -> (a -> m b)
      -> m b

A monad’s bind, written between: c >>= f is f of what c gives, as do writes x <- c then f x.

instanceMonadMaybe

instance instanceMonadMaybe : Monad Maybe

Maybe’s monad: a computation that may give nothing, and then the rest gives nothing too.

instanceMonadEither

instance instanceMonadEither : {e : Type} -> Monad (Either e)

Either e’s monad: a computation that may fail with an e (Left), and then the rest fails with it too.

traverse

traverse : {m : Type -> Type}
         -> {{mo : Monad m}}
         -> {a b : Type}
         -> (a -> m b)
         -> List a
         -> m (List b)

f of each element, in order, and the list of what they gave.

>>> traverse (mo := instanceMonadMaybe) (\x -> if x > 0 then Just (x * 2) else Nothing) [1, 2, 3]
Just [2, 4, 6]
>>> traverse (mo := instanceMonadMaybe) (\x -> if x > 0 then Just x else Nothing) [1, -2, 3]
Nothing

foldM

foldM : {m : Type -> Type}
      -> {{mo : Monad m}}
      -> {a b : Type}
      -> (b -> a -> m b)
      -> b
      -> List a
      -> m b

A left fold, each step a computation: f z x1, then f of what it gave and x2, and so on.

>>> foldM (mo := instanceMonadMaybe) (\acc x -> if x > 0 then Just (acc + x) else Nothing) 0 [1, 2, 3]
Just 6

when

when : {m : Type -> Type} -> {{mo : Monad m}} -> Bool -> m Unit -> m Unit

c if b, else nothing done.

>>> when (mo := instanceMonadMaybe) False Nothing
Just MkUnit

unless

unless : {m : Type -> Type} -> {{mo : Monad m}} -> Bool -> m Unit -> m Unit

c unless b: if b, nothing done.

>>> unless (mo := instanceMonadMaybe) False Nothing
Nothing

replicateM

replicateM : {m : Type -> Type}
           -> {{mo : Monad m}}
           -> {a : Type}
           -> Int
           -> m a
           -> m (List a)

c, n times (none, for n not above 0), and the list of what it gave each time.

>>> replicateM (mo := instanceMonadEither) 3 (Right 'x' : Either String Rune)
Right ['x', 'x', 'x']

Id

type Id a = a

The identity monad: a value is its own computation. Pure code written as statements is run do ..., whose do is taken apart by this monad’s idBind and idPure: their calls simplified away, each of its loops a function calling only itself, giving its variables back.

run

run : {a : Type} -> Id a -> a

the value of a computation of the identity monad: run do ...

idPure

idPure : {a : Type} -> a -> Id a

idBind

idBind : {a b : Type} -> Id a -> (a -> Id b) -> Id b

typeOf

typeOf : {a : Type} -> a -> Type

the type of x: what a do block’s loop takes its variable x as, and what x := e checks e against

inferred

inferred : {a : Type} -> Unit -> Type

a type its uses decide, the implicit argument left to be solved: what a do block’s loop gives, and what let mut x = e checks e against

leaveScope

leaveScope : {a : Type} -> (Unit -> a) -> a

What a scope’s answer says to do once it is left, done: a do block’s try and with go on so, to what follows them or further out.

++

(++) : {a : Type} -> List a -> List a -> List a

xs ++ ys: the elements of xs, then those of ys.

>>> [1, 2] ++ [3]
Cons 1 (Cons 2 (Cons 3 Nil))

Iterate

theory Iterate c where
  Elem : Type
  Cursor : Type
  start : c -> Cursor
  next : Cursor -> Maybe (Elem, Cursor)

What for x in c do ... goes through: a cursor over c’s elements (each an Elem), from where it starts, each step the next element and the cursor after it, or nothing at the end. A list’s cursor is the list, an array’s its index, a range’s what is left of it.

iterateOf

iterateOf : {c : Type} -> {{it : Iterate c}} -> c -> Iterate c

the instance of Iterate found for x’s type: what a for over x goes through it by

instanceIterateList

instance instanceIterateList : {a : Type} -> Iterate (List a)

A list, from its first element.

Range

data Range = MkRange Int Int

The integers from one to another, both of them in, as for goes through them (none, if the second is less than the first).

range

range : Int -> Int -> Range

instanceIterateRange

instance instanceIterateRange : Iterate Range

A range, from its first integer up.

strByteAt

strByteAt : String -> Int -> Int

strFromByte

strFromByte : UInt8 -> String

byteAt

byteAt : String -> Int -> Int

The byte at i, 0 to 255; out of range, -1.

>>> byteAt "a\u{e9}" 1
195
>>> byteAt "a\u{e9}" 3
-1

fromByte

fromByte : UInt8 -> String

The string of one byte: a byte of no rune too, which no literal but a \xNN escape has. An Int is made a byte by uint8’s fromInt, wrapping around (fromByte (U8.fromInt n)).

>>> fromByte 104 ^ fromByte 105
"hi"
>>> fromByte 255 == "\xff" && byteAt (fromByte 0) 0 == 0
True

strRunes

strRunes : String -> List Rune

strOfRunes

strOfRunes : List Rune -> String

strRuneAt

strRuneAt : String -> Int -> Rune

strRuneWidth

strRuneWidth : String -> Int -> Int

runeToInt

runeToInt : Rune -> Int

uint8FromInt

uint8FromInt : Int -> UInt8

runes

runes : String -> List Rune

The runes of s, its code points, UTF-8 read: runes "a😀" is ['a', '😀']; what is not UTF-8 is U+FFFD, one for each longest start of a rune’s bytes (or a byte that starts none), as TextDecoder reads it. Their operations are rune’s.

fromRunes

fromRunes : List Rune -> String

The string of runes, UTF-8 (one that is no Unicode scalar value, U+FFFD): fromRunes (runes s) is s, where s is UTF-8.

RuneAt

type RuneAt = { rune : Rune, width : Int }

A rune of a string, and how many bytes of it it takes.

runeAt

runeAt : String -> Int -> RuneAt

The rune whose bytes start at i, and how many they are (Go’s utf8.DecodeRuneInString): where they are not UTF-8, U+FFFD, as runes reads it; out of range, U+FFFD of none.

>>> (runeAt "a\u{e9}b" 1).width
2
>>> (runeAt "a\u{e9}b" 2).width
1

instanceIterateString

instance instanceIterateString : Iterate String

A string, rune by rune, as runes reads it: its cursor is the string and the byte its next rune starts at.

compareString

compareString : String -> String -> Ordering

The order of two strings, their bytes’ (of UTF-8, their runes’), by one comparison of them.

>>> (MkPair (compareString "pear" "apple") (compareString "pear" "pears") : Pair Ordering Ordering)
MkPair GT LT
>>> compareString "z" "\u{e9}"
LT

orderByCompare

orderByCompare : {a : Type}
               -> {{eq : Equality a}}
               -> (a -> a -> Ordering)
               -> Order a

The Order of a comparison and the type’s equality: lt and le are by the comparison.

instanceOrderString

instance instanceOrderString : Order String

Strings’ order, their bytes’ (compareString’s).

>>> "apple" < "pear" && not ("pear" <= "pea")
True

instanceOrderBool

instance instanceOrderBool : Order Bool

False before True.

>>> compare (False : Bool) True
LT

instanceOrderUnit

instance instanceOrderUnit : Order Unit

instanceOrderOrdering

instance instanceOrderOrdering : Order Ordering

LT before EQ before GT.

instanceOrderList

instance instanceOrderList : {a : Type} -> {{ord : Order a}} -> Order (List a)

Lists by their elements, the first that differ (a list before a longer one it begins).

>>> (MkPair (compare ([1, 2] : List Int) [1, 3]) (compare ([1, 2] : List Int) [1]) : Pair Ordering Ordering)
MkPair LT GT
>>> (instanceOrderList : Order (List Int)).eq.equal [1, 2] [1, 2]
True

instanceOrderMaybe

instance instanceOrderMaybe : {a : Type} -> {{ord : Order a}} -> Order (Maybe a)

Nothing before any Just, and those by what they hold.

instanceOrderPair

instance instanceOrderPair : {a b : Type}
                           -> {{ordA : Order a}}
                           -> {{ordB : Order b}}
                           -> Order (a, b)

Pairs by their first, then their second.

>>> compare (MkPair 1 "b" : Pair Int String) (MkPair 1 "a")
GT

indexOf

indexOf : String -> String -> (from : Int) -> Maybe Int

Where needle is first in s, from byte from on (from 0, a from below it), if it is.

>>> indexOf "lo" "hello, world: lo" 0
Just 3
>>> indexOf "lo" "hello, world: lo" 4
Just 14
>>> indexOf "," "a,b,c" (from := 2)
Just 3
>>> indexOf "" "ab" 2
Just 2
>>> indexOf "" "ab" 3
Nothing

contains

contains : String -> String -> Bool

>>> contains "ell" "hello" && not (contains "elo" "hello")
True

startsWith

startsWith : (prefix : String) -> String -> Bool

endsWith

endsWith : String -> String -> Bool

split

split : String -> String -> List String

The pieces of s between the seps (not empty: split "," "a,,b" is ["a", "", "b"]).

>>> split ", " "a, b, , c"
Cons "a" (Cons "b" (Cons "" (Cons "c" Nil)))

joinWith

joinWith : String -> List String -> String

The strings, with sep between each two.

lines

lines : String -> List String

The pieces of s between its line breaks ("\n").

>>> lines "one\ntwo\n"
Cons "one" (Cons "two" (Cons "" Nil))

unlines

unlines : List String -> String

isSpaceCode

isSpaceCode : Int -> Bool

words

words : String -> List String

The pieces of s between its spaces, tabs and line breaks.

unwords

unwords : List String -> String

skipSpaces

skipSpaces : String -> Int -> Int -> Int

trim

trim : String -> String

Without the spaces at either end.

parseInt

parseInt : String -> Maybe Int

A decimal integer (42, -7), if s is one, whole.

foldBytes

foldBytes : {a : Type} -> (a -> Int -> a) -> a -> String -> a

The bytes, each 0 to 255, from the first, into z; no list of them made, as runes would make one (rune’s foldl goes through the runes so).

>>> foldBytes (\n b -> n * 2 + b % 2) 0 "ab\xff"
5

byteString

byteString : Int -> String

mapBytes

mapBytes : (Int -> Int) -> String -> String

Each byte f of it, given 0 to 255 (and what it gives wrapped around to that, as uint8’s fromInt wraps): as long a string, no list of its bytes made, but the string itself grown, in place, as ^ grows one.

>>> mapBytes (\b -> if 97 <= b && b <= 122 then b - 32 else b) "heff, \u{e9}!"
"HEFF, \u{e9}!"
>>> mapBytes (\b -> b + 1) "\xff\x00a"
"\x00\x01b"

withCodePoint

withCodePoint : String -> Int -> String

mapRunes

mapRunes : (Rune -> Rune) -> String -> String

Each rune f of it, the runes read as runes reads them (what is not UTF-8, U+FFFD) and written as fromRunes writes them: fromRunes (List.map f (runes s)), but no list made, the string grown, in place, as ^ grows one.

>>> mapRunes (\c -> if c == 'a' then '\u{3bb}' else c) "a\xffb\u{e9}"
"\u{3bb}\u{FFFD}b\u{e9}"
>>> mapRunes (\c -> c) "\xe9\x80" == fromRunes (runes "\xe9\x80")
True

floatOfDecimal

floatOfDecimal : Int -> String -> Int -> Int -> Float64

The float, of 64 bits or 32 (n), nearest the decimal strSlice s i j — a -, digits, perhaps a point and digits, perhaps an exponent (2.5, -1e-7, 12.5E+3), nothing else — rounded once, a tie to the even, as std.math’s fromDecimal and float32’s round m times 10 to the power e; of text that is no such decimal, NaN, as no decimal is. parseFloat and float32’s parseFloat32 read a whole string so.

parseFloat

parseFloat : String -> Maybe Float64

The float nearest the decimal s is, whole (2.5, -1e-7), as floatOfDecimal reads one, if it is one: correctly rounded, as a float literal is.

>>> parseFloat "0.1"
Just 0.1
>>> parseFloat "-0"
Just (-0.0)
>>> parseFloat "2.4703282292062328e-324"
Just 5.0e-324
>>> parseFloat "1e400"
Just Infinity
>>> parseFloat "1."
Nothing

Debug

theory Debug a where
  debug : a -> String

A type’s values as the source writes them — a string quoted, debug "hi" is "\"hi\"", a rune debug 'a' is "'a'", bytes a literal — so that two values that differ are not written the same: what a test shows a value as and compares two by (check’s assertEqual, forAll), as Rust’s Debug and Python’s repr are. The prelude’s instances are of Int, Float64, String, Rune, Bytes, Bool, Unit and Ordering, and of a List, a Maybe, a Pair and an Either of types that have one; a fixed-width type’s is its module’s.

debug

debug : {a : Type} -> {{shows : Debug a}} -> a -> String

The value written as its type’s instance writes it.

showInt

showInt : Int -> String

An Int as a literal writes it, Int’s debug.

>>> showInt 42 ^ " " ^ showInt (-7)
"42 -7"

showFloat

showFloat : Float64 -> String

A Float64 as a literal writes it, Float64’s debug: the fewest digits that read back as it, a point among them, an exponent beyond 1e21 and below 1e-6, and -0.0 with its sign — read as a literal, the very float. What no literal is, as it is: NaN, Infinity, -Infinity.

>>> showFloat 2.5
"2.5"
>>> showFloat (neg 0.0) ^ " " ^ showFloat 1.0e23 ^ " " ^ showFloat 5.0e-324
"-0.0 1.0e23 5.0e-324"
>>> showFloat 100.0 ^ " " ^ showFloat 1.0e-7
"100.0 1.0e-7"

instanceDebugInt

instance instanceDebugInt : Debug Int

instanceDebugFloat64

instance instanceDebugFloat64 : Debug Float64

>>> debug 42 ^ " " ^ debug (-7) ^ " " ^ debug 2.5
"42 -7 2.5"

instanceDebugString

instance instanceDebugString : Debug String

Quoted, its ", \ and line feeds escaped.

>>> debug "say \"hi\"\n"
"\"say \\\"hi\\\"\\n\""
>>> debug "hi"
"\"hi\""

instanceOrderRune

instance instanceOrderRune : Order Rune

Runes by their code points.

>>> 'a' < 'b' && compare 'z' 'a' == GT
True

instanceDebugRune

instance instanceDebugRune : Debug Rune

A rune as a literal writes it, quoted: a control character an escape, one that is no scalar value as U+FFFD (as Go’s %q).

>>> debug 'a' ^ " " ^ debug '\'' ^ " " ^ debug '\n' ^ " " ^ debug '\u{1b}'
"'a' '\\'' '\\n' '\\u{1b}'"

bytesToList

bytesToList : Bytes -> List UInt8

uint8ToInt

uint8ToInt : UInt8 -> Int

instanceDebugBytes

instance instanceDebugBytes : Debug Bytes

Bytes as a binary writes them, b[...]: each run of printable ASCII, a byte from 32 up to 126, a string (" and \ escaped), and any other byte its number.

>>> debug b[10, "GET \"\\", 195, 169]
"b[10, \"GET \\\"\\\\\", 195, 169]"
>>> debug b[]
"b[]"

instanceDebugBool

instance instanceDebugBool : Debug Bool

instanceDebugUnit

instance instanceDebugUnit : Debug Unit

instanceDebugOrdering

instance instanceDebugOrdering : Debug Ordering

>>> debug (True : Bool) ^ " " ^ debug (MkUnit : Unit) ^ " " ^ debug (GT : Ordering)
"True MkUnit GT"

instanceDebugList

instance instanceDebugList : {a : Type} -> {{shows : Debug a}} -> Debug (List a)

>>> debug ([1, 2] : List Int)
"[1, 2]"
>>> debug ([["a"], []] : List (List String))
"[[\"a\"], []]"

instanceDebugMaybe

instance instanceDebugMaybe : {a : Type}
                            -> {{shows : Debug a}}
                            -> Debug (Maybe a)

>>> debug (Just [1] : Maybe (List Int)) ^ " " ^ debug (Nothing : Maybe Int)
"Just ([1]) Nothing"

instanceDebugPair

instance instanceDebugPair : {a b : Type}
                           -> {{showsA : Debug a}}
                           -> {{showsB : Debug b}}
                           -> Debug (a, b)

>>> debug (MkPair 1 "one" : Pair Int String)
"MkPair (1) (\"one\")"

instanceDebugEither

instance instanceDebugEither : {a b : Type}
                             -> {{showsA : Debug a}}
                             -> {{showsB : Debug b}}
                             -> Debug (Either a b)

>>> debug (Left 1 : Either Int String) ^ " " ^ debug (Right "1" : Either Int String)
"Left (1) Right (\"1\")"

Show

theory Show a where
  show : a -> String

A type’s values as text, for a reader rather than for the source — a string itself, a rune its one-rune string, bytes the text they are — as Rust’s Display and Python’s str are, beside Debug (Rust’s Debug, Python’s repr). The prelude’s instances are of String, Rune and Bytes, and of Int, Float64, Bool, Unit and Ordering, written as debug writes them; a fixed-width type’s is its module’s, as debug writes it too. A List, a Maybe, a Pair and an Either have none: there is no one text of them.

show

show : {a : Type} -> {{text : Show a}} -> a -> String

The value as its type’s instance makes it text.

instanceShowString

instance instanceShowString : Show String

Itself.

>>> show "hi"
"hi"

instanceShowRune

instance instanceShowRune : Show Rune

The string of it alone, fromRunes [c] (Go’s string(c)).

>>> show 'a'
"a"

bytesToString

bytesToString : Bytes -> String

instanceShowBytes

instance instanceShowBytes : Show Bytes

The text of them, UTF-8, what is not UTF-8 U+FFFD, as rune’s toValid makes it (and TextDecoder reads it).

>>> show b["h", 0xc3, 0xa9, 0xff, "i"]
"hé\u{FFFD}i"

instanceShowInt

instance instanceShowInt : Show Int

instanceShowFloat64

instance instanceShowFloat64 : Show Float64

>>> show 42 ^ " " ^ show (-7) ^ " " ^ show 2.5
"42 -7 2.5"

instanceShowBool

instance instanceShowBool : Show Bool

instanceShowUnit

instance instanceShowUnit : Show Unit

instanceShowOrdering

instance instanceShowOrdering : Show Ordering

>>> show (True : Bool) ^ " " ^ show (MkUnit : Unit) ^ " " ^ show (GT : Ordering)
"True MkUnit GT"

onWindows

onWindows : Unit -> Bool

Whether the program runs on Windows: as the system it is built for says — a C program, the target zig builds it for; in JavaScript, Node.js’s process.platform (False in a page). The same all through a run, so a function of no effect; std.path reads a path in the style it says.

Coe

theory Coe from to where
  coe : from -> to

A value of one type taken as one of another, without saying so: where an expression of type from is given and a to is expected, and the two do not unify, heff puts in coe, by the one instance of Coe from to in scope (as any instance argument is found). Both types must be known whole there; one coercion is put in, never two in a row. The prelude has one, instanceCoeLazy: a module that has a type made from another declares its own, as std.path does Coe String Path.

coe

coe : {from to : Type} -> {{coerces : Coe from to}} -> from -> to

The value taken as a to, as its instance takes it: what heff puts in where a coercion is wanted.

instanceCoeLazy

instance instanceCoeLazy : {a : Type} -> Coe ~a a

A Lazy a, ~a, where an a is expected: forced.

bitsEq

bitsEq : Bits -> Bits -> Bool

bitsLength

bitsLength : Bits -> Int

bitsIntAt

bitsIntAt : Bits -> Int -> Int -> Int -> Int

bitsOfInt

bitsOfInt : Int -> Int -> Int -> Bits

bitsConcat

bitsConcat : List Bits -> Bits

bitsSlice

bitsSlice : Bits -> Int -> Int -> Bits

bitsOfBytes

bitsOfBytes : Bytes -> Bits

bitsBytes

bitsBytes : Bits -> Bytes

floatBits

floatBits : Int -> Float64 -> Int

floatOfBits

floatOfBits : Int -> Int -> Float64

runeFromInt

runeFromInt : Int -> Rune

bitsSized

bitsSized : Int -> Bits -> Bits

The first n bits of b, as a segment x::bits-size(n) writes them: of fewer, abandoned.

bitsHasBytesAt

bitsHasBytesAt : Bits -> Int -> Bytes -> Bool

Whether the bytes s are those of b at bit o.

>>> bitsHasBytesAt (bitsConcat [bitsOfInt 4 0 1, bitsOfBytes b["hi"]]) 4 b["hi"]
True

CodePoint

theory CodePoint a where
  codePoint : a -> Int

What a segment of utf8, utf16 or utf32 writes: a code point, an Int’s or a Rune’s.

instanceCodePointInt

instance instanceCodePointInt : CodePoint Int

instanceCodePointRune

instance instanceCodePointRune : CodePoint Rune

codePointOf

codePointOf : {a : Type} -> {{point : CodePoint a}} -> a -> Int

The code point of a value of CodePoint.

isScalarValue

isScalarValue : Int -> Bool

Whether c is a Unicode scalar value: from 0 up to U+10FFFF, but the surrogates.

utf8Bytes

utf8Bytes : Int -> Bytes

The code point c as UTF-8, as a segment c::utf8 writes it: what is no scalar value, abandoned.

>>> bytesToList (bytesConcat [utf8Bytes 65, utf8Bytes 233, utf8Bytes 8364, utf8Bytes 128512])
[65, 195, 169, 226, 130, 172, 240, 159, 152, 128]

utf16Bytes

utf16Bytes : Int -> Int -> Bytes

The code point c as UTF-16, as a segment c::utf16 writes it, its units as the flags f say (1 little-endian): what is no scalar value, abandoned.

utf32Bytes

utf32Bytes : Int -> Int -> Bytes

The code point c as UTF-32: what is no scalar value, abandoned.

utf8Count

utf8Count : Int -> Int

utf8Lead

utf8Lead : Int -> Int

utf8Least

utf8Least : Int -> Int

utf8Rest

utf8Rest : (Int -> Int) -> Int -> Int -> Int -> Int

utf8CodeBy

utf8CodeBy : (Int -> Int) -> Int -> Int

utf8WidthOf

utf8WidthOf : Int -> Int -> Int

utf8WidthBy

utf8WidthBy : (Int -> Int) -> Int

bytesByteAt

bytesByteAt : Bytes -> Int -> Int -> Int

bitsByteAt

bitsByteAt : Bits -> Int -> Int -> Int

bytesUtf8Width

bytesUtf8Width : Bytes -> Int -> Int

How many bits the UTF-8 code point at bit o of b is, as a segment c::utf8 reads it: where there is none (a byte that is no continuation, too few, a surrogate, one written longer than it is), 0.

>>> ([bytesUtf8Width b["a", 0xc3, 0xa9] 0, bytesUtf8Width b["a", 0xc3, 0xa9] 8, bytesUtf8Width b[0xc3, 0x28] 0, bytesUtf8Width b[0xed, 0xa0, 0x80] 0, bytesUtf8Width b[0xc0, 0x80] 0, bytesUtf8Width b[0xc3] 0] : List Int)
[8, 16, 0, 0, 0, 0]

bitsUtf8Width

bitsUtf8Width : Bits -> Int -> Int

bytesUtf8At

bytesUtf8At : Bytes -> Int -> Rune

The UTF-8 code point at bit o of b, there.

bitsUtf8At

bitsUtf8At : Bits -> Int -> Rune

utf16WidthBy

utf16WidthBy : (Int -> Int) -> Int

utf16CodeBy

utf16CodeBy : (Int -> Int) -> Int

bytesUnitAt

bytesUnitAt : Bytes -> Int -> Int -> Int -> Int

bitsUnitAt

bitsUnitAt : Bits -> Int -> Int -> Int -> Int

bytesUtf16Width

bytesUtf16Width : Bytes -> Int -> Int -> Int

How many bits the UTF-16 code point at bit o of b is, its units as the flags f say: where there is none, 0.

bitsUtf16Width

bitsUtf16Width : Bits -> Int -> Int -> Int

bytesUtf16At

bytesUtf16At : Bytes -> Int -> Int -> Rune

The UTF-16 code point at bit o of b, there.

bitsUtf16At

bitsUtf16At : Bits -> Int -> Int -> Rune

instanceEqualityBits

instance instanceEqualityBits : Equality Bits

Bits’ (their other operations are bits’s): the same bits.

>>> bitsOfInt 3 0 5 == bitsConcat [bitsOfInt 1 0 1, bitsOfInt 2 0 1]
True
>>> bitsOfBytes b[1, 2] == bitsOfInt 16 0 258
True

instanceDebugBits

instance instanceDebugBits : Debug Bits

Bits as a binary writes them: their whole bytes as bytes are (instanceDebugBytes), then the bits left, v::k — or, none left, b[]::bits, so that what is written is Bits again.

>>> debug (bitsConcat [bitsOfBytes b["GET"], bitsOfInt 3 0 5])
"b[\"GET\", 5::3]"
>>> debug (bitsOfBytes b[1, 2]) ^ " " ^ debug (bitsOfBytes b[]) ^ " " ^ debug (bitsOfInt 1 0 1)
"b[1, 2, b[]::bits] b[b[]::bits] b[1::1]"

instanceShowBits

instance instanceShowBits : Show Bits

Their bits, each 0 or 1.

>>> show (bitsOfInt 5 0 21)
"10101"

natrec

natrec : {c : Type} -> c -> (Nat -> c -> c) -> Nat -> c

Recursion on Nat, non-dependent.

>>> natrec (c := Nat) Zero (\_ n -> Succ (Succ n)) (Succ (Succ Zero))
Succ (Succ (Succ (Succ Zero)))