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.
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.