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: Rewriting countability and finiteness #83

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

WIP: Rewriting countability and finiteness #83

wants to merge 1 commit into from

Conversation

CohenCyril
Copy link
Member

@CohenCyril CohenCyril commented Apr 25, 2018 •
edited
Loading

countability and finiteness now share the interface of countType and finType through the coercions countable >-> Sortclass and finite >-> Sortclass
e.g. rpickle c is replaced by @pickle [countType of c] where c : countable E.
Additionally, sketching lemmas about combining infinite, finite and cofinite sets.

This is a draft, it does not compile anymore, but it sketches improvements of countability theory.

@CohenCyril CohenCyril added experiment 🧪 This issue/PR is very experimental refactoring labels Apr 25, 2018
@CohenCyril CohenCyril requested a review from strub April 25, 2018 21:34
@CohenCyril
WIP: Rewriting countability and finiteness
f5e466c 
countability and finiteness now share the interface of countType and finType through the coercions countable >-> Sortclass and finite >-> Sortclass
e.g. rpickle c is replaced by @Pickle [countType of c] where c : countable E.
Additionally, sketching lemmas about combining infinite, finite and cofinite sets.
@CohenCyril CohenCyril marked this pull request as draft September 25, 2020 12:34
@CohenCyril CohenCyril removed the request for review from strub September 25, 2020 12:34
@affeldt-aist
Copy link
Member

memo: mentioned in PR #294

@affeldt-aist
Copy link
Member

partially handed by PR #435?

@affeldt-aist affeldt-aist added renaming/refactoring 🔧 This is about a renaming or refactoring in the library and removed kind: refactoring labels Mar 15, 2023
@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
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
experiment 🧪 This issue/PR is very experimental renaming/refactoring 🔧 This is about a renaming or refactoring in the library 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
No milestone
Development

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