[Agda] --rewriting and the Agda standard library

[Siek, Jeremy]

On Apr 23, 2020, at 9:01 PM, Matthew Daggitt <matthewdaggitt at gmail.com<mailto:matthewdaggitt at gmail.com>> wrote:

Hi Jeremy,
 As the error message says, the `-- rewriting` flag is not compatible <https://agda.readthedocs.io/en/v2.6.1/language/safe-agda.html#safe-agda> with the `--safe` flag, and (as one would hope!) the standard library uses `--safe` flag extensively.

As you say, passing the flag via the command line applies it to all files, and therefore setting `--rewriting` in such a manner is not compatible with the standard library. In contrast, as the `-- rewriting` flag is neither infective nor co-infective<https://agda.readthedocs.io/en/v2.6.1/tools/command-line-options.html?highlight=infective#consistency-checking-of-options-used>, adding it via an OPTIONS pragma only applies it to that file.

Very good, thank you!

Cheers,
Jeremy

__________________________________________
Jeremy G. Siek    <jsiek at indiana.edu<mailto:jsiek at indiana.edu>>
Professor
Luddy School of Informatics, Computing, and Engineering
Indiana University Bloomington
http://homes.soic.indiana.edu/jsiek/






-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200424/9043d8da/attachment.html>