diff options
| author | Hugo Herbelin | 2018-09-25 16:41:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-25 16:41:23 +0200 |
| commit | 1624fdddeb6078621a5741927491d07a8219607c (patch) | |
| tree | e6ecf910a585a015eb86ac464e63ec4396c71f8f | |
| parent | 7eb8a7eb8d23ffaf149f71a46fb1b089b90db7f8 (diff) | |
| parent | 31a52b8e1efc85aead31af1ea4a8106c4c28ffba (diff) | |
Merge PR #8235: NArith: deprecate N2Bv_gen
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | theories/NArith/Ndigits.v | 8 |
2 files changed, 9 insertions, 0 deletions
@@ -91,6 +91,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. |