Jacques Carette
Jacques Carette
Re: Algebra.Construct.Sub 'mis-identification', and #2852 -- those are not yet released, so there is still time! And yes, I hope that @Taneb will chyme in soon. I think it is...
What the most ergonomic construction of `ℤ` is unknown to me. All the versions that I've seen develop dark corners or are ridiculously tedious to work with. Probably because we're...
In `div-mod`: make that `go` a private global, having it in a where clause will mean that proving anything about `div-mod` will be very hard. And yes, the INT construction...
I would be curious as to the scale of the knock-ons. For both. These are certainly excellent questions to ask. I can't help but think that, in practice, this won't...
Will review 'soon' - first have to fix the broken CI. So there will be a delay.
(closing and reopening to get the CI to run)
There are issues with nameless proofs. First, usability: goals become giant. Second, because Agda is fairly eager to delta and eta expand, some record fields do end up duplicated. So...
There's a conflict now - could you resolve it please?