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.

Sign up for GitHub

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

Jump to bottom

WIP: eudoxus reals #116

Draft
wants to merge 17 commits into
base: master
Choose a base branch
from
Draft

WIP: eudoxus reals #116

wants to merge 17 commits into from

Conversation

strub
Copy link
Member

@strub strub commented Oct 17, 2018

Because it's fun.

@drouhling drouhling mentioned this pull request Oct 31, 2018
Closed
10 tasks
@affeldt-aist affeldt-aist added this to the 0.3.4 milestone Nov 9, 2020
@affeldt-aist affeldt-aist modified the milestones: 0.3.4, 0.3.5 Dec 12, 2020
@affeldt-aist affeldt-aist modified the milestones: 0.3.5, 0.3.6 Dec 21, 2020
@affeldt-aist
Copy link
Member

We should maybe merge this one. @strub Do you want to squash some of the last commits which do not look informative? ("merge remote-tracking...", commit without commit message, "merge branch 'master'...)

@affeldt-aist affeldt-aist modified the milestones: 0.3.6, 0.3.7 Mar 4, 2021
@affeldt-aist
Copy link
Member

We should maybe merge this one.

Sorry, I didn't realize it was not yet completed. Or are the Admitted's irrelevant?

@affeldt-aist affeldt-aist modified the milestones: 0.3.7, 0.3.8 Mar 31, 2021
@affeldt-aist affeldt-aist modified the milestones: 0.3.8, 0.3.9 May 29, 2021
@affeldt-aist affeldt-aist modified the milestones: 0.6.3, 0.6.4 Jun 20, 2023
@affeldt-aist affeldt-aist added the experiment 🧪 This issue/PR is very experimental label Jul 28, 2023
@affeldt-aist affeldt-aist modified the milestones: 0.6.4, 0.6.5 Jul 28, 2023
@affeldt-aist affeldt-aist modified the milestones: 0.6.5, 0.6.6 Sep 27, 2023
@affeldt-aist
Copy link
Member

Maybe this could help: https://www.isa-afp.org/entries/Eudoxus_Reals.html

@affeldt-aist affeldt-aist modified the milestones: 0.6.6, 0.6.7 Nov 7, 2023
@affeldt-aist affeldt-aist modified the milestones: 0.6.7, 0.6.8 Jan 1, 2024
@affeldt-aist affeldt-aist modified the milestones: 0.7.0, 1.0.0 Jan 17, 2024
@affeldt-aist affeldt-aist modified the milestones: 1.0.0, 1.1.0 Jan 24, 2024
@proux01 proux01 added the TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. label Jan 25, 2024
@affeldt-aist affeldt-aist modified the milestones: 1.1.0, 1.2.0 Mar 26, 2024
@affeldt-aist affeldt-aist modified the milestones: 1.2.0, 1.3.0 May 27, 2024
@affeldt-aist affeldt-aist modified the milestones: 1.3.0, 1.4.0 Jul 24, 2024
@affeldt-aist affeldt-aist modified the milestones: 1.4.0, 1.5.0 Sep 19, 2024
@affeldt-aist affeldt-aist modified the milestones: 1.5.0, 1.6.0 Oct 7, 2024
@affeldt-aist affeldt-aist mentioned this pull request Oct 14, 2024
Merged
@affeldt-aist affeldt-aist modified the milestones: 1.6.0, 1.7.0 Oct 24, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
enhancement ✨ This issue/PR is about adding new features enhancing the library experiment 🧪 This issue/PR is very experimental TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done.
Projects
None yet
Milestone
1.7.0
Development

Successfully merging this pull request may close these issues.
4 participants
@strub @affeldt-aist @CohenCyril @proux01