Skip to content

Commit 5e0a71c

Browse files
coqbot-app[bot]proux01
coqbot-app[bot]
and
proux01
authored
Merge PR #18947: deprecate Bvector
Reviewed-by: proux01 Co-authored-by: proux01 <[email protected]>
2 parents c5614d0 + fea8e82 commit 5e0a71c

File tree

2 files changed

+29
-1
lines changed

2 files changed

+29
-1
lines changed

‎doc/changelog/11-standard-library/18947-deprecate-Bvector.rst‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
- **Deprecated:** ``Bool.Bvector``. Users are encouraged to consider ``list bool`` instead. Please open an issue if you would like to keep using ``Bvector``.
2+
(`#18947 <https://github.com/coq/coq/pull/18947>`_,
3+
by Andres Erbsen).

‎theories/Bool/Bvector.v‎

Lines changed: 26 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,8 @@
1010

1111
(** N.B.: Using this encoding of bit vectors is discouraged.
1212
See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v>. *)
13-
Attributes warn(cats="stdlib vector", note="Using Vector.t is known to be technically difficult, see <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v>.").
13+
Attributes deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.").
14+
Local Set Warnings "-deprecated".
1415

1516
(** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *)
1617

@@ -50,53 +51,72 @@ NOTA BENE: all shift operations expect predecessor of size as parameter
5051
(they only work on non-empty vectors).
5152
*)
5253

54+
#[deprecated(since="8.20", note="Consider [list bool] instead. Please open an issue if you would like to keep using Bvector.")]
5355
Definition Bvector := Vector.t bool.
5456

57+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
5558
Definition Bnil := @Vector.nil bool.
5659

60+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
5761
Definition Bcons := @Vector.cons bool.
5862

63+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
5964
Definition Bvect_true := Vector.const true.
6065

66+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
6167
Definition Bvect_false := Vector.const false.
6268

69+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
6370
Definition Blow := @Vector.hd bool.
6471

72+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
6573
Definition Bhigh := @Vector.tl bool.
6674

75+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
6776
Definition Bsign := @Vector.last bool.
6877

78+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
6979
Definition Bneg := @Vector.map _ _ negb.
7080

81+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
7182
Definition BVand := @Vector.map2 _ _ _ andb.
7283

84+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
7385
Definition BVor := @Vector.map2 _ _ _ orb.
7486

87+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
7588
Definition BVxor := @Vector.map2 _ _ _ xorb.
7689

90+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
7791
Definition BVeq m n := @Vector.eqb bool eqb m n.
7892

93+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
7994
Definition BshiftL (n:nat) (bv:Bvector (S n)) (carry:bool) :=
8095
Bcons carry n (Vector.shiftout bv).
8196

97+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
8298
Definition BshiftRl (n:nat) (bv:Bvector (S n)) (carry:bool) :=
8399
Bhigh (S n) (Vector.shiftin carry bv).
84100

101+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
85102
Definition BshiftRa (n:nat) (bv:Bvector (S n)) :=
86103
Bhigh (S n) (Vector.shiftrepeat bv).
87104

105+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
88106
Fixpoint BshiftL_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
89107
match p with
90108
| O => bv
91109
| S p' => BshiftL n (BshiftL_iter n bv p') false
92110
end.
93111

112+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
94113
Fixpoint BshiftRl_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
95114
match p with
96115
| O => bv
97116
| S p' => BshiftRl n (BshiftRl_iter n bv p') false
98117
end.
99118

119+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
100120
Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
101121
match p with
102122
| O => bv
@@ -108,10 +128,15 @@ End BOOLEAN_VECTORS.
108128
Module BvectorNotations.
109129
Declare Scope Bvector_scope.
110130
Delimit Scope Bvector_scope with Bvector.
131+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
111132
Notation "^~ x" := (Bneg _ x) (at level 35, right associativity) : Bvector_scope.
133+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
112134
Infix "^&" := (BVand _) (at level 40, left associativity) : Bvector_scope.
135+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
113136
Infix "^⊕" := (BVxor _) (at level 45, left associativity) : Bvector_scope.
137+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
114138
Infix "^|" := (BVor _) (at level 50, left associativity) : Bvector_scope.
139+
#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
115140
Infix "=?" := (BVeq _ _) (at level 70, no associativity) : Bvector_scope.
116141
Open Scope Bvector_scope.
117142
End BvectorNotations.

0 commit comments

Comments
 (0)