Axiom

Axioms or postulates are used to introduce new terms or types without defining them. This is done using the axiom keyword.

axiom <name> : <type>;

Usage

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:

axiom A : Type;

axiom x : A;

Important Considerations

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.