Skip to content

Built-ins

Juvix has support for the built-in natural numbers 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

builtin IO
axiom IO : Type;

builtin nat-print
axiom printNat : Nat → IO;