Jacques Carette
Jacques Carette
I was thinking it would be done incrementally, i.e. simply start by allowing `.lagda` as input. In fact, we should take a serious look at all of the 1lab's infrastructure...
Agreed, once there is such a fresh issue, this one should be closed.
Unfortunately the PR itself is regarded as a breaking change (even though not doing this for v2.0 was an oversight), so this issue should also get that label.
Yes, I think that that name makes more sense than `.New`. I'll implement that.
Just to be clear, I've asked @Sofia-Insa to "port" some things from a library of mine to stdlib. That library was developed with a slightly different context in mind, which...
Yes, we should absolutely generalize this to an arbitrary setoid. And indeed, the bijection is enough to prove no duplication. Note that since `Fin n` has decidable equality, setoid `A`...
That's an excellent point. Ok, I have to agree, as I've witnessed "subtly wrong" sufficiently many times. Sigh.
I've converted this PR to Draft, so that it can be augmented to be more full-featured regarding (at least) finite enumerability.
Another one that I should take over. I most definitely want to continue pushing on this.
Next couple of weeks? Unfortunately not so likely, sorry.