diff options
Diffstat (limited to 'theories/NArith/Ndigits.v')
| -rw-r--r-- | theories/NArith/Ndigits.v | 8 |
1 files changed, 8 insertions, 0 deletions
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. |