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

Compatibility with std++ ? #20

Open
spitters opened this issue Mar 21, 2020 · 3 comments
Open

Compatibility with std++ ? #20

spitters opened this issue Mar 21, 2020 · 3 comments

Comments

@spitters
Copy link

spitters commented Mar 21, 2020

A gitter discussion suggested making stdlib2 compatible with stdpp. Is that a realistic goal?

@robbertkrebbers @RalfJung

@robbertkrebbers
Copy link

I don't follow the Coq Gitter, so can you remind us what this discussion was about exactly? And what do you mean by compatible?

@Zimmi48
Copy link
Contributor

Zimmi48 commented Mar 21, 2020

@spitters I also don't know what you mean by compatible but the goal is indeed that stdlib2 will take whatever is relevant from stdpp and that the rest will be ported on top of it to test its validity (same thing for math-comp and compcert).

@spitters
Copy link
Author

So far, stdlib2 seems to be mostly following the math-comp style. stdpp uses a different style (type classes, for example).
E.g. how do we expect the finmap library to look?

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

No branches or pull requests

3 participants