Built-in types and operators

Primitive types

Type	Description	Literals
`Nat`	Natural numbers (unsigned integers)	`0`, `42`
`Int`	Signed 64-bit integers — since 2.0-alpha	`-7`, or `42` where an `Int` is expected
`Bool`	Booleans	`true`, `false`
`String`	UTF-8 text	`"hello"`
`Unit`	Unit type, one value	`()`

Operators

Arithmetic — on `Nat` or `Int`

Both operands have the same type; there is no implicit conversion.

Operator	On `Nat`	On `Int`
`+`	Addition	Addition; traps on overflow
`-`	Subtraction, saturating at `0`	Subtraction; traps on overflow
`*`	Multiplication	Multiplication; traps on overflow
`/`	Division	Division, truncating toward zero; traps on a zero divisor
`%`	Remainder	Remainder, with the dividend’s sign; traps on a zero divisor
`-x`	Refused	Negation; traps on overflow

A trap prints one line — error: integer overflow in + — and ends the program, the same way in the interpreter and in a compiled binary.

Conversions — built in

Function	Description
`to_int(n: Nat) -> Int`	The same number as an `Int`; traps above the largest `Int`
`from_int(i: Int) -> Nat`	The same number as a `Nat`; a negative value becomes `0`

See Signed integers.

Comparison — yield `Bool`

Operator	Description
`==`	Equality
`!=`	Inequality
`<`	Less than
`>`	Greater than
`<=`	Less than or equal
`>=`	Greater than or equal

Logical — on `Bool`

Operator	Description
`&&`	AND
`\|\|`	OR

Strings

Operator	Description
`++`	Concatenation

Both operands of ++ must already be String; convert a Nat first — there is no built-in conversion, so write one. To build a string from many pieces, use the runtime’s StringBuilder, which is reached through extern "C" rather than built in.

Where precedence is not obvious, parenthesise.

Conventional types

There is no standard library yet, so these are not in scope until you declare them — using Option without a type Option<T> = … line is refused with cannot find type 'Option' in this scope. They are the definitions every program in these pages, and the compiler’s own source, uses:

Type	Definition
`Option<T>`	`None \| Some(T)`
`Result<T, E>`	`Ok(T) \| Err(E)`
`List<T>`	`Nil \| Cons(T, List<T>)`
`Pair<A, B>`	`MkPair(A, B)`
`Ordering`	Comparison outcome

Constructor order is significant to the compiler’s encoding — the first constructor is the left alternative. Keep the conventional order when defining your own.

Form	Description
`Eq<T, a, b>`	The proposition that `a` equals `b` at type `T`
`refl`	Proof of `x = x`; lower-case
`sym(p)`	Flips an equality proof
`trans(p, q)`	Chains two equality proofs
`cong(f, p)`	Congruence
`subst(a, b, c)`	Substitution / rewriting
`natind(motive, base, step, n)`	Induction over naturals
`natrec(type, base, step, n)`	Primitive recursion over naturals

See Proofs.

Keywords

The words below cannot be used as names — not for a function, a parameter or a binding. Using one fails to parse, and the error is reported at the token after it, so fn f(sym: Nat) points at Nat.

Group	Words
Core	`fn let if else match return try type struct enum true false`
Proof — the ones that catch people	`theorem lemma axiom by have show assume forall exists Prop sorry refl subst sym trans cong natind natrec`
Type	`Bool Nat Unit Void`
Module	`mod pub`
Reserved for later	`async await use impl trait where self Self mut ref move loop while for in break continue const static extern crate super dyn unsafe as`

use, extern and as are in the last row but already mean what the rest of these pages say they mean. albite explain keywords prints the compiler’s own table, and albite explain keywords <name> answers for one word.