<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<br class="">
<div><br class="">
<blockquote type="cite" class="">
<div class="">On Apr 23, 2020, at 9:01 PM, Matthew Daggitt <<a href="mailto:matthewdaggitt@gmail.com" class="">matthewdaggitt@gmail.com</a>> wrote:</div>
<br class="Apple-interchange-newline">
<div class="">
<div dir="ltr" class="">Hi Jeremy,
<div class=""> As the error message says, the `-- <span style="font-variant-ligatures:no-common-ligatures" class="">
rewriting</span>` flag is not <a href="https://agda.readthedocs.io/en/v2.6.1/language/safe-agda.html#safe-agda" class="">
compatible </a>with the `--safe` flag, and (as one would hope!) the standard library uses `--safe` flag extensively.</div>
<div class=""><br class="">
</div>
<div class="">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 `--
<span style="font-variant-ligatures:no-common-ligatures" class="">rewriting</span>` flag is neither
<a href="https://agda.readthedocs.io/en/v2.6.1/tools/command-line-options.html?highlight=infective#consistency-checking-of-options-used" class="">
infective nor co-infective</a>, adding it via an OPTIONS pragma only applies it to that file.<br class="">
</div>
</div>
</div>
</blockquote>
<div><br class="">
</div>
<div>Very good, thank you!</div>
<div><br class="">
</div>
<div>Cheers,</div>
<div>Jeremy</div>
</div>
<br class="">
<div class="">
<div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div style="color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div style="color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div style="color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div class=""><span style="font-family: Menlo; font-size: medium; orphans: 2; widows: 2;" class="">__________________________________________</span><br style="font-family: Menlo; orphans: 2; widows: 2;" class="">
<span style="font-family: Menlo; orphans: 2; widows: 2;" class="">Jeremy G. Siek <<a href="mailto:jsiek@indiana.edu" class="">jsiek@indiana.edu</a>></span><br style="font-family: Menlo; orphans: 2; widows: 2;" class="">
<span style="font-family: Menlo; orphans: 2; widows: 2;" class="">Professor</span><br style="font-family: Menlo; orphans: 2; widows: 2;" class="">
<span style="font-family: Menlo; orphans: 2; widows: 2;" class="">Luddy School of Informatics, Computing, and Engineering</span><br style="font-family: Menlo; orphans: 2; widows: 2;" class="">
<span style="font-family: Menlo; orphans: 2; widows: 2;" class="">Indiana University Bloomington</span><br style="font-family: Menlo; orphans: 2; widows: 2;" class="">
<span style="font-family: Menlo; orphans: 2; widows: 2;" class=""><a href="http://homes.soic.indiana.edu/jsiek/" class="">http://homes.soic.indiana.edu/jsiek/</a></span><br class="">
</div>
<div class=""><span style="font-family: Menlo; orphans: 2; widows: 2;" class=""><br class="">
</span></div>
</div>
</div>
<br class="Apple-interchange-newline">
</div>
<br class="Apple-interchange-newline">
</div>
<br class="Apple-interchange-newline">
<br class="Apple-interchange-newline">
</div>
<br class="">
</body>
</html>