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