Skip to content

Conversation

jamesmckinna
Copy link
Contributor

@jamesmckinna jamesmckinna commented Jul 2, 2023

See the discussion on issue #1919.

Two Three parts to this:

  • low-hanging fruit: added pattern synonym and consequences/uses of it to Data.Nat.*
  • higher-hanging fruit: reconcile the two definitions of _∣_ for the Data.Nat.Base.*-rawMagma instance
  • knock-on changes for Data.Integer.Divisibility.* and Data.Rational.* only if the preceding step succeeds

Proposal: merge the low-hanging fruit one now, and keep this branch, and the above checkboxes, open for a subsequent independent PR. In the meantime, a chance to think about the pro/contra proposals regarding how to reconcile the various definitions...

Copy link
Contributor

@JacquesCarette JacquesCarette left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The code up to this point of completion makes sense to me and seems to be a clear improvement.

@jamesmckinna
Copy link
Contributor Author

Label status:ready as a placeholder for 'enough commits from my side' ;-)

Copy link
Contributor

@JacquesCarette JacquesCarette left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Continues to be nice.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants