agda-stdlib

agda-stdlib copied to clipboard

[ refactor ] Fix/rationalise 'legacy' binder names in `Relation.Binary.Definitions` (and elsewhere?)

1

Seeing #2546 made me realise that I personally can no longer tolerate the inconsistency between the use of `x` (in `Reflexive`), `x` and `y` (in `Symmetric`), but `i` `j` and...

jamesmckinna

[ refactor ] Reconcile left/right congruence statements and proofs

12

> Have now added revised types for the new lemmas, and note the following: * `++⁺ʳ` now has a type corresponding to the *explicitly* quantified version of `Algebra.Definitions.LeftCongruent` * `++⁺ˡ`...

jamesmckinna