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;