[Agda] --rewriting and the Agda standard library

[Jesper Cockx]

Hi Jeremy,

How exactly is --rewriting incompatible with the standard library? It's
true that it does not use --rewriting, but you can always import a file
that does not use --rewriting from one that does (the other way around is
more problematic).

-- Jesper

On Thu, Apr 23, 2020 at 10:11 PM Siek, Jeremy <jsiek at indiana.edu> wrote:

>
> From a quick test run, it seems that --rewriting is incompatible with most
> if not
> all of the standard library. Is that correct? I was hoping to use
> --rewriting,
> but using the standard library is rather more important.
>
> Cheers,
> Jeremy
>
> __________________________________________
> Jeremy G. Siek    <jsiek at indiana.edu>
> Professor
> Luddy School of Informatics, Computing, and Engineering
> Indiana University Bloomington
> http://homes.soic.indiana.edu/jsiek/
>
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200423/99b5ae46/attachment.html>