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

Decide for natural numbers whether x < y or y ≤ x #1279

Merged
merged 1 commit into from
Feb 5, 2025

Conversation

lowasser
Copy link
Contributor

@lowasser lowasser commented Feb 5, 2025

The rationals have it, but the naturals don't.

@EgbertRijke
Copy link
Collaborator

Some of these things are also addressed in #1211, but your PR is certainly very welcome!

@EgbertRijke
Copy link
Collaborator

To be a bit more specific, #1211 doesn't touch on the rational numbers, but it vastly expands everything about the naturals. The revisions I am making there have triggered some wider changes across the library, which is why it hasn't converged to a finished PR yet (I admit, that this is bad style on my part).

@EgbertRijke EgbertRijke merged commit 26f7289 into UniMath:master Feb 5, 2025
4 checks passed
@lowasser lowasser deleted the decide-le-leq-natural branch February 5, 2025 22:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants