[Agda] --rewriting and the Agda standard library

[Jesper Cockx]

What I meant with "more problematic" is that it is possible to have
expressions that are well-typed with --rewriting but ill-typed without, so
if you import such a term from a file that uses --rewriting then you end up
with an ill-typed term. So making --rewriting infective would probably be a
good idea.

-- Jesper

On Fri, Apr 24, 2020 at 11:32 AM Nils Anders Danielsson <nad at cse.gu.se>
wrote:

> On 2020-04-24 03:01, Matthew Daggitt wrote:
> > the `-- rewriting` flag is neither infective nor co-infective
>
> Doesn't it make sense for this flag to be infective? Jesper stated that
> "the other way around is more problematic". I opened an issue for this
> (https://github.com/agda/agda/issues/4621).
>
> --
> /NAD
> _______________________________________________
> 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/20200424/012ad176/attachment.html>