Great. Thank you for the pointer, James. On Fri, Jul 3, 2020 at 1:22 PM James Wood <james.wood.100 at strath.ac.uk> wrote: > > Okay, then probably this is the relevant issue: > https://github.com/agda/agda/issues/59 . > I know there have been a lot of changes to termination checking > involving `with`, because it seems very hard to do it right. > > James