Axiom

Axioms or postulates can be introduced by using the axiom keyword. For example, let us imagine one wants to write a program that assumes A is a type, and there exists a term x that inhabits A. Then the program would look like the following.

-- Example.juvix
module Example;
 axiom A : Type;
 axom x : A;
end;

Terms introduced by the axiom keyword lack any computational content. However, it is possible to attach computational content to an axiom by giving compilation rules, see the compile keyword.