diff options
| author | Yishuai Li | 2018-07-26 22:23:13 -0400 |
|---|---|---|
| committer | Yishuai Li | 2018-09-07 21:56:44 -0400 |
| commit | 46c0756406beea84564625c423e9c5f2307689e1 (patch) | |
| tree | b4da05621e766b5f454a0b32d1e69878ed3ca098 | |
| parent | 69fb545f0fad2b356f5be1ce3e1a24b5afe26ce2 (diff) | |
Bvector: add BVeq and some notations
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | theories/Bool/Bvector.v | 11 |
2 files changed, 14 insertions, 0 deletions
@@ -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. |