[ refactor ] use variables in Algebra.Consequences.Base
#2592
Conversation
jamesmckinna
changed the title
variables in Algebra.Consequences.Base
|
Hmmm... recent merge conflicts were a bit strange, hopefully fixed now. |
| @@ -1848,7 +1848,7 @@ m∸n≤∣m-n∣ m n with ≤-total m n | |||
| n ∸ m ∎ | |||
|
|
|||
| *-distribˡ-∣-∣ : _*_ DistributesOverˡ ∣_-_∣ | |||
| *-distribˡ-∣-∣ a = wlog ≤-total (comm⇒sym[distribˡ] {_◦_ = _*_} ∣-∣-comm a) | |||
| *-distribˡ-∣-∣ a = wlog ≤-total (comm⇒sym[distribˡ] ∣-∣-comm {_◦_ = _*_} a) | |||
There was a problem hiding this comment.
This makes this look like not a cosmetic change but a breaking change? And therefore needs to be a v3.0 if we want to do it?
There was a problem hiding this comment.
Sigh.
The proof above was itself only introduced last week in #2577 ... and I guess that it is inevitable that the move to using variable always has the potential to reorder the order of implicit arguments in proofs. In the past we haven't (apparently? it typically has arisen where there has been a ground argument lifted out as a variable, eg an element of the Carrier of a Setoid, n : ℕ etc. and in general those have been inferrable, so we haven't observed the 'problem') regarded such as breaking behaviour...
But here, it's possibly because the 'real' underlying issue may be that the ambient parameterisation on the binary operation ought to be explicit (cf. Function.Consequences.Propositional). Will investigate whether there's a better fix to the above.
There was a problem hiding this comment.
You're probably right it should be v3.0, and then we can fix the parametrisation problems exposed above as well.
There was a problem hiding this comment.
... and I'd press on the argument in favour of #2572 as well as part of such v3.0 changes...
This lifts out the refactoring aspects of #2572 and should be merged first of the two.
It also rectifies two bugs
Data.Rational.Unnormalised.Propertiesvariables means that the names of implicit parameters now matter; butBasestill used the incorrect symbol for the binary operation, which has now been corrected.NB One (and only one!) knock-on change needed when supplying an implicit
Op₂parameter!UPDATED: in the
Propositionalcase, instantiating proofs fromSetoidwith instances ofcongshould be accompanied by a change in parametrisation from implicit to explicit, because (PropositionalEquality.Core.)congcan't (necessarily) infer its argument, whereas the typechecker can infer_∙_when deploying generalSetoidproofs taking an explicitcong : Congruent₂ _∙_argument ...