Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add %? operator #4696

Open
lehins opened this issue Oct 15, 2024 · 2 comments
Open

Add %? operator #4696

lehins opened this issue Oct 15, 2024 · 2 comments
Assignees
Labels
🍰 good first issue Good for newcomers enhancement New feature or request

Comments

@lehins
Copy link
Collaborator

lehins commented Oct 15, 2024

There are many places where we protect against zero denominator when constructing a rational that has a property x % 0 == 0. We should create a helper function %? that takes care of this use case for us and use it in all places where this use case occurs.

@lehins lehins added enhancement New feature or request 🍰 good first issue Good for newcomers labels Oct 15, 2024
@Soupstraw Soupstraw self-assigned this Jan 7, 2025
@Soupstraw
Copy link
Contributor

Soupstraw commented Jan 7, 2025

I started on this, but I think it'd be better to add a new type NonZeroRational which can only be constructed from a non-zero rational. Then %? can have the type Rational -> NonZeroRational -> Rational.

The reason that I think this'll be better is that we often divide by totalStake so if we changed the type of totalStake to NonZeroRational, we'd only have to prove that it's non-zero once and then we can divide by that however many times we want.

@Soupstraw
Copy link
Contributor

Ok, I also tried the other approach, but I don't think there's a nice way to do it, so I'll just use Maybe.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
🍰 good first issue Good for newcomers enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

2 participants