diff options
| author | Yishuai Li | 2018-09-07 21:22:11 -0400 |
|---|---|---|
| committer | Yishuai Li | 2018-09-07 21:23:54 -0400 |
| commit | 31a52b8e1efc85aead31af1ea4a8106c4c28ffba (patch) | |
| tree | 1cbdc4516ce9b89735fbf4a2e954251b0816040d | |
| parent | 69fb545f0fad2b356f5be1ce3e1a24b5afe26ce2 (diff) | |
NArith: deprecate N2Bv_gen
Use N2Bv_sized instead.
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | theories/NArith/Ndigits.v | 8 |
2 files changed, 9 insertions, 0 deletions
@@ -64,6 +64,7 @@ Standard Library want). - Added `Ndigits.N2Bv_sized`, and proved some lemmas about it. + Deprecated `Ndigits.N2Bv_gen`. - The scopes `int_scope` and `uint_scope` have been renamed to `dec_int_scope` and `dec_uint_scope`, to clash less with ssreflect diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 68a98e4292..a2a2430e91 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -578,6 +578,7 @@ Qed. (** To state nonetheless a second result about composition of conversions, we define a conversion on a given number of bits : *) +#[deprecated(since = "8.9.0", note = "Use N2Bv_sized instead.")] Fixpoint N2Bv_gen (n:nat)(a:N) : Bvector n := match n return Bvector n with | 0 => Bnil @@ -705,3 +706,10 @@ Proof with simpl; auto. destruct (Bv2N n v) as [|[]]; rewrite <- IHv... Qed. + +Lemma N2Bv_N2Bv_sized_above (a : N) (k : nat) : + N2Bv_sized (N.size_nat a + k) a = N2Bv a ++ Bvect_false k. +Proof with auto. + destruct a... + induction p; simpl; f_equal... +Qed. |