Jacques Carette
Jacques Carette
I don't yet have a concrete suggestion on how to make it easy to have named modules for the corresponding record in Agda - but I have started thinking about...
Apparently it's not that simple?
I saw that 1.7.1 was released just earlier today - I was just under the impression that the CI would grab the latest. If it doesn't, then something else needs...
I wasn't going to upgrade, but I also won't refuse a ready-made PR that makes it all work!
The CI liked it. I'm still vaguely reluctant. Opinions?
I'm going to pull in a few more PRs first, and then merge-and-bump.
The PRs that I wanted to pull in are in. I just have not had any time to devote to this in the last few weeks. Looks like the next...
> I'd be more than happy to help out! Great - see your email for more.
@Boarders this was really good - a couple of small changes, and it's ready to go in. Will you be able to do there? Or would like us to?
No worries! I'm patient and not in a hurry. Don't strain your knee for this.