From 46c0756406beea84564625c423e9c5f2307689e1 Mon Sep 17 00:00:00 2001
From: Yishuai Li
Date: Thu, 26 Jul 2018 22:23:13 -0400
Subject: Bvector: add BVeq and some notations

---
 CHANGES                 |  3 +++
 theories/Bool/Bvector.v | 11 +++++++++++
 2 files changed, 14 insertions(+)

diff --git a/CHANGES b/CHANGES
index 5d1c9a9c2d..2780bce9c1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -92,6 +92,9 @@ Standard Library
   impacts users running Coq without the init library (`-nois` or
   `-noinit`) and also issuing `Require Import Coq.Init.Datatypes`.
 
+- Added `Bvector.BVeq` that decides whether two `Bvector`s are equal.
+- Added notations for `BVxor`, `BVand`, `BVor`, `BVeq` and `BVneg`.
+
 Tools
 
 - Coq_makefile lets one override or extend the following variables from
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index aecdb59dbe..4eb05d12f1 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -70,6 +70,8 @@ Definition BVor := @Vector.map2 _ _ _ orb.
 
 Definition BVxor := @Vector.map2 _ _ _ xorb.
 
+Definition BVeq m n := @Vector.eqb bool eqb m n.
+
 Definition BshiftL (n:nat) (bv:Bvector (S n)) (carry:bool) :=
   Bcons carry n (Vector.shiftout bv).
 
@@ -99,3 +101,12 @@ Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
 
 End BOOLEAN_VECTORS.
 
+Module BvectorNotations.
+Delimit Scope Bvector_scope with Bvector.
+Notation "^~ x" := (Bneg _ x) (at level 35, right associativity) : Bvector_scope.
+Infix    "^&"   := (BVand  _) (at level 40, left  associativity) : Bvector_scope.
+Infix    "^⊕"   := (BVxor  _) (at level 45, left  associativity) : Bvector_scope.
+Infix    "^|"   := (BVor   _) (at level 50, left  associativity) : Bvector_scope.
+Infix    "=?"   := (BVeq _ _) (at level 70, no    associativity) : Bvector_scope.
+Open Scope Bvector_scope.
+End BvectorNotations.
-- 
cgit v1.2.3