You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Hmm I'd be tempted to have the standard signature ℚ → ℤ for those operations then have another operator frac : ℚ →ℚ that returns the fractional part. Presumably they're simply going to be implemented by the _/_ and _%_ operators respectively so it's not like they have any computational overlap.
I've just opened a PR #1585 which implements the suggested functions. I have not been able to prove any properties about said functions. Should we open a new issue for the implementation of those properties?
This interesting article suggests useful operations we may want to have on rational numbers:
together with the proofs of their properties, of course.
The text was updated successfully, but these errors were encountered: