search

coq-community / manifesto

Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.
Other
68 stars 6 forks source link

Proposal to move dedekind-reals to Coq-community #156

Closed palmskog closed 3 weeks ago

palmskog commented 3 weeks ago

Project name: dedekind-reals

Initial author(s): Andrej Bauer, Vincent Semeria

Current URL: https://github.com/andrejbauer/dedekind-reals

Kind: pure Coq library

License: MIT

Description: A formalization of Dedekind real numbers. Unlike the formalization of Dedekind reals in Coq's standard library, this formalization is based on Coq's Prop; a comparison can be viewed here.

Status: maintained by @andrejbauer, but proposed to be moved to Coq-community for more collaborative maintenance and preservation.

andrejbauer commented 3 weeks ago

I would like to thank @palmskog for making sure the library does not rot into oblivion. I am of course deligthed to have the library included in the Coq-community.

andrejbauer commented 3 weeks ago

I have transferred the ownership to Coq-community.

andrejbauer commented 3 weeks ago

I nominate @VincentSe to be a maintainer of the library, as he contributed large chunks of it and should be considered a co-author.

palmskog commented 3 weeks ago

Thanks @andrejbauer, since the transfer is done I will close this issue.

@VincentSe if you want to be a maintainer of the library, please let me know (e.g., here on GitHub) and I will add you as admin to the dedekind-reals repository.