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

Left/Right inconsistency

Open JacquesCarette opened this issue 10 months ago • 1 comments

Issue #2532 from @jamesmckinna draws our attention to some of the left/right inconsistencies. There are... more. I attach two lists (courtesy of @jmougeot ), one which details definitions that use subscript r and l (rather than the majority superscript), and also other items that use either Left or Right in their names, or 'r'/'l' superscripts (or even both!!). And these are just definition sites, not all lines. There are quite a lot of these. So I am rather at a loss on how to check 'consistency' when the scale is this large. But at least now we have the raw data in hand.

JacquesCarette avatar Mar 12 '25 01:03 JacquesCarette

Heroic work, but indeed: words fail me as to how we might reconcile all this!

jamesmckinna avatar Mar 12 '25 08:03 jamesmckinna