agda-stdlib icon indicating copy to clipboard operation
agda-stdlib copied to clipboard
verified publisher icon agda

Orientation of the equation `Algebra.Properties.RingWithoutOne.-‿distribˡ-*`

Open jamesmckinna opened this issue 5 months ago • 5 comments

It seems we got this wrong when we added it (and its right-hand sibling):

  • it's defined by an outermost appeal to sym
  • its 5 uses in stdlib are all bracketed by an outermost appeal to sym

Perhaps there's nothing to be done (hypothetical-rewrite?), but it's... ironic.

jamesmckinna avatar Aug 12 '25 11:08 jamesmckinna

We ought to be able to fix design mistakes!

I participated in one release of Maple where we fixed a lot of design mistakes. Users grumbled for a bit, and then just adopted the new version. [It did help that we wrote something that fixed a lot of things semi-automatically, even if it wasn't perfect.]

JacquesCarette avatar Aug 22 '25 18:08 JacquesCarette

I guess a v3.0 breaking PR is in order then!? Or could one argue for a 'bug fix' one?

jamesmckinna avatar Aug 23 '25 03:08 jamesmckinna

The question is: are design bugs considered bugs? And what's the line between a design bug and a sub-optimal design?

JacquesCarette avatar Aug 27 '25 14:08 JacquesCarette

The question is: are design bugs considered bugs? And what's the line between a design bug and a sub-optimal design?

Good questions! We should try to agree answers as part of our library-design policy/philosophy?

jamesmckinna avatar Aug 29 '25 04:08 jamesmckinna

I've added a "maintainer's meeting agenda" section to the Wiki and created a page for our to-be-scheduled next meeting.

JacquesCarette avatar Aug 29 '25 14:08 JacquesCarette