Axioms or postulates are used to introduce new terms or types without defining
them. This is done using the
axiom <name> : <type>;
Consider a scenario where you want to create a program that assumes A as a type, and there exists a term x that belongs to this type A. The syntax for such a program would be as follows:
It is crucial to understand that terms introduced by the
axiom keyword do not
contain any computational content. This implies that they are merely abstract
concepts without any inherent operational value.
Consequently, programs that include axioms (which are not marked as builtins) cannot be compiled to most targets.