Jacques Carette
Jacques Carette
From the code you show, the argument order seems fine? Is there something I'm missing? It also seems to me that it is `*-cancelʳ-≤-neg` that is weird, not what you've...
I'm still not quite getting it. `o m n` is a bizarre order, `m n o` is better. But that's just order of the variables. You probably mean something deeper...
I think this PR is a good unit of progress as-is.
I definitely agree with @Taneb that we need proceed carefully. Unfortunately, I don't have enough experience formalizing Algebra are these parts (`IntegralSemiring`, etc) so I don't have reliable opinions on...
I agree that it feels inconsistent. Normally, I'd go for implicit when practice shows that it can often be inferred - but it turns out that practice is very mixed...
If we make it "normal style" to use ` _` (i.e. space-underscore) when it can be, then explicit is pretty light-weight.
Since this is indeed 'intra' v2.1, I think this is the way to go.
Let me understand if I've understood this right. The context here seems to be that some modules introduces fundamental functionality (sometimes highly parametrized), while other modules are 'actually' creating a...
`TotalSemiDecidable` for the name of the *abstract property* seems fine. As a root for the naming convention for 'instances', I agree that it is awful. `decYes` ? As in 'decide...
I wouldn't quite use 'deprecate' to describe the situation, although I think we agree on the core: we have to opportunity to benefit from dependent types here, and yet by...