Compatibility with std++ ?

Open spitters opened this issue 5 years ago • 3 comments

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

@robbertkrebbers @RalfJung

Mar 21 '20 10:03 spitters

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?

Mar 21 '20 10:03 robbertkrebbers

@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).

Mar 21 '20 13:03 Zimmi48

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?

Mar 21 '20 15:03 spitters