builtin

The types the language answers with itself: every other module imports this one without writing it.

Bool

data Bool = True | False

what a comparison answers, and what if, && and || take

Unit

data Unit = MkUnit

what a thunk is forced with

List

data List a = Nil | Cons a (List a)

what [a, b] is, and what an array is made from and turned into

Lazy

data Lazy a

what ~A is: an A computed only where it is forced, force, and once, kept for the next time; ~e delays e. Its tag is no one else’s: a Lazy is made by ~e alone

force

force : {a : Type} -> ~a -> a

the value, computed the first time it is forced and kept: where an a is expected, a Lazy a given is forced without saying so (the prelude’s Coe (Lazy a) a)

int8Eq

int8Eq : Int8 -> Int8 -> Bool

the equalities of the fixed-width types: what a literal pattern of one is matched by (as one of an Int is by the prelude’s intEq), and what their modules (int32 and the others) name

int16Eq

int16Eq : Int16 -> Int16 -> Bool

int32Eq

int32Eq : Int32 -> Int32 -> Bool

int64Eq

int64Eq : Int64 -> Int64 -> Bool

uint8Eq

uint8Eq : UInt8 -> UInt8 -> Bool

uint16Eq

uint16Eq : UInt16 -> UInt16 -> Bool

uint32Eq

uint32Eq : UInt32 -> UInt32 -> Bool

uint64Eq

uint64Eq : UInt64 -> UInt64 -> Bool

float32Eq

float32Eq : Float32 -> Float32 -> Bool

runeEq

runeEq : Rune -> Rune -> Bool

the equality of runes, by code point: what a rune literal pattern is matched by, and what rune names