Should we archive this repository now that stdlib has a bits type? I don't think stdlib implements every single thing that bbv does, but it's been enough for guru and bedrock2 and fiat-crypto. Thus, I think that a future development needing bitvector support would be better of exenting bits than using bbv word. And maybe we can stop maintaining this repository.
Nothing in Rocq CI depends on the target for this repo: gitlab.inria.fr/coq/coq/-/pipelines/1286380
@samuelgruetter @JasonGross @gmalecha @achlipala wdyt?
Should we archive this repository now that stdlib has a bits type? I don't think stdlib implements every single thing that bbv does, but it's been enough for guru and bedrock2 and fiat-crypto. Thus, I think that a future development needing bitvector support would be better of exenting
bitsthan using bbvword. And maybe we can stop maintaining this repository.Nothing in Rocq CI depends on the target for this repo: gitlab.inria.fr/coq/coq/-/pipelines/1286380
@samuelgruetter @JasonGross @gmalecha @achlipala wdyt?