search

coq / stdlib2

GNU Lesser General Public License v2.1
39 stars 9 forks source link

Compatibility with std++ ? #20

Open spitters opened 4 years ago

spitters commented 4 years ago

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

@robbertkrebbers @RalfJung

robbertkrebbers commented 4 years ago

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 commented 4 years ago

@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 commented 4 years ago

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?