Skip to content


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.

module axioms;

axiom A : Type;

axiom x : A;

Terms introduced by the axiom keyword lack any computational content. Programs containing axioms not marked as builtins cannot be compiled to most targets.