agda-stdlib
agda-stdlib copied to clipboard
Left/Right inconsistency
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.
- Subscripts: lower.txt
- Left/Right: matches.txt
Heroic work, but indeed: words fail me as to how we might reconcile all this!