Jacques Carette
Jacques Carette
Looks like we should close this issue now - right @gallais and @MatthewDaggitt ? Or is there some back-porting to master that should be done first?
I think you are correct @jamesmckinna . But there must also be something very slightly different about them? Perhaps some subtlety about irrelevance?
I think you're right about all of this being redundant. I think the main remaining point is around findability and naming: 1. Neither @Taneb nor Sergei were able to find...
> retraining people to define their record values using copatterns rather than record { ... } syntax. I would seriously object to being forced to retrain myself this way. I...
Thanks for the clarification - I had not seen that subtlety. I don't use matching on records very often, I'm fine with being retrained to do it even less.
In my opinion, what is needed is that the source of the library use `Commutative` etc, even some of the weirder ones, but when users inspect the type of those...
The `.Example` idea is indeed quite good. If such a convention is adopted (i.e. the tooling supports it), then it would be best to let the examples develop organically. I...
That level of 'documentation' would be worth putting in the PR, including adding some to the current Partiality monad.
I think the first refactor makes a lot of sense. The second refactor scares me. Basically because of the indirection through `with`: this makes goals extremely hard to work with....
I'd say - 'on the nose' subsets are a pain in dependent type theory, because they need to be encoded via a predicate - subsets of X encoded as (Y,...