Skip to content

Built-ins

Juvix has support for the built-in natural type and a few functions that are compiled to efficient primitives.

Built-in inductive definitions

builtin nat
type Nat :=
| zero : Nat
| suc : Nat Nat;

Builtin function definitions

syntax operator + additive;

builtin nat-plus
+ : Nat Nat Nat
| zero b := b
| (suc a) b := suc (a + b);

Builtin axiom definitions

module example-print-nat;
builtin IO
axiom IO : Type;

builtin nat-print
axiom printNat : Nat IO;
end;