[Agda] --rewriting and the Agda standard library

Nils Anders Danielsson nad at cse.gu.se
Fri Apr 24 11:31:28 CEST 2020


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


More information about the Agda mailing list