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¶
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;