search

adampetcher / fcf

Foundational Cryptography Framework for machine-checked proofs of cryptography.
Other
48 stars 23 forks source link

do not depend on Coq.Bool.Bvector #47

Closed andres-erbsen closed 6 months ago

andres-erbsen commented 6 months ago

I am investigating whether we could remove Bvector (specialization of Vector to Bool) from stdlib. This is the part that FCF actually uses.

Feel free to ignore for now or merge right away.