diff options
| -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. |