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