Andreas Abel

I pressed Ctrl-C after maybe a couple hundred lines of `Checking Foo` with a repeating pattern. I am packing the material which reproduces this, but its more than 300MB, will...

Material is here: http://www.cse.chalmers.se/~abela/tmp/agda-issue-5245/index.html

> After a while the following message is printed repeatedly @nad, does this mean "several times" or did you have to interrupt? I am asking for clarification because both issues...

@jespercockx @L-TChen The progress here is stuck on the last question, it seems... > parameters are not regarded as arguments, so the LHS of this rule is matched successfully. Is...

Modality subsumption `@erased

@jake-87 wrote: > Performing a case split on `b` in either hole (`C-c C-c b RET`) produces the following error... Wouldn't a better behavior be that you get the dot...

Related: - #2183 - #3964

@topikettunen, thanks for investigating! There are basically 3 ways to proceed. 1. Just leave the deprecation warnings in and worry about them once the functions get actually removed. 2. Use...

Rebased onto latest master. Since we dropped testing with GHC 7, I see no obstacle in merging this now...

Added CI to update CI to ubuntu-20.04 (necessary). Ping @thoughtpolice