By using the option
--safe (as a pragma option, or on the
command-line), a user can specify that Agda should ensure that
features leading to possible inconsistencies should be disabled.
Here is a list of the features
--safe is incompatible with:
postulate; can be used to assume any axiom.
--allow-unsolved-metas; forces Agda to accept unfinished proofs.
--allow-incomplete-matches; forces Agda to accept unfinished proofs.
--no-positivity-check; makes it possible to write non-terminating programs by structural “induction” on non strictly positive datatypes.
--no-termination-check; gives loopy programs any type.
--injective-type-constructors; together with excluded middle leads to an inconsistency via Chung-Kil Hur’s construction.
--irrelevant-projections; enables potentially unsound irrelevance features (irrelevant levels, irrelevant data matching, and projection of irrelevant record fields, respectively).
--rewriting; turns any equation into one that holds definitionally. It can at the very least break convergence.
primEraseEqualityprimitive together with
primEraseEquality, one can derive the K axiom.
--allow-exec; allows system calls during type checking.
--no-load-primitives; allows the user to bind the sort and level primitives manually.