Jacques Carette
Jacques Carette
It's annoying to have to 'help' the inferencer so much, but it has the huge advantage of being coherent with other `Pointwise`, so I'm in favour of that.
@gallais can you update the gist please? I think I'm going to spend some of my time working on this.
I hope that @Saransh-cpp was using `README/Design/Fixity.agda` to set the fixities (I thought a reference to that file was here in the comments, but not so, only inside the linked...
If you're happy to "bless" this fixity guide then yes, probably should be integrated into the style guide.
I will attempt to look at the gist seriously as soon as I can. Still buried with many other things on my plate.
Yes, #2386 did update the documentation. I was going to continue slowing picking at this issue until it's done. Yes, it is getting trickier!
I'm completely for consistency. And your reasoning is great. And yet, I'm not sure I really like `⁻¹` as the solution. Basically I think it boils down to 'inversion' being...
If I had to guess, I'd say that the underscores in `Functors _ _` are likely greatly contributing. I wouldn't at all be surprised that Agda decided to eta-expand the...
Just dropping by here to add my +1. I've now seen some very compelling uses in both Haskell and in Idris, and am now jealous. Edward Kmett's Linear Logic library...