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¶
infixl 6 +; builtin nat-plus + : Nat → Nat → Nat; + zero b := b; + (suc a) b := suc (a + b);
Builtin axiom definitions¶
open import Stdlib.System.IO; builtin nat-print axiom printNat : Nat → IO;