do not depend on Coq.Bool.Bvector

adampetcher · Apr 15, 2024 · 33a49dc · 33a49dc
1 parent 291f500
commit 33a49dc
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 0 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -5,6 +5,7 @@ src/FCF/Array.v
 src/FCF/Asymptotic.v
 src/FCF/Bernoulli.v
 src/FCF/Blist.v
+src/FCF/Bvector.v
 src/FCF/Class.v
 src/FCF/Comp.v
 src/FCF/CompFold.v

diff --git a/src/FCF/Bvector.v b/src/FCF/Bvector.v
@@ -0,0 +1,6 @@
+Require Coq.Vectors.Vector.
+Export Bool Vector.VectorNotations.
+
+Definition Bvector := Vector.t bool.
+Definition Bvect_false := Vector.const false.
+Definition BVxor := @Vector.map2 _ _ _ xorb.