agda/doc/user-manual/language/safe-agda.lagda.rst
Lines 11 to 15 in 3a9d389
By using the option :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 :option:`--safe` is incompatible with:In the list following here, only postulates and certain options are mentioned, but not the pragmas ruled out by
--safe
, e.g.
TERMINATING
,
NO_UNIVERSE_CHECK
etc.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4