diff options
| author | Hugo Herbelin | 2018-09-26 19:22:51 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-26 19:22:51 +0200 |
| commit | 71296e6e91de5b3fea08ef4b34426a02304f00b8 (patch) | |
| tree | 2594f723fb04d1e13adb09bf6f45ac247d0081d5 | |
| parent | f49928874b51458fb67e89618bb350ae2f3529e4 (diff) | |
| parent | 46c0756406beea84564625c423e9c5f2307689e1 (diff) | |
Merge PR #8171: 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
@@ -133,6 +133,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. |