diff options
| author | Yishuai Li | 2018-10-29 13:21:08 -0400 |
|---|---|---|
| committer | Yishuai Li | 2018-10-29 13:23:07 -0400 |
| commit | fb56c4eb9cb4afe4365c05e0cc6ba2643064ee6b (patch) | |
| tree | 672f09fc5d1504f5b47adb792ae4a733a4bba631 | |
| parent | e4c95253e01992bee0786312a5e2bbc5ec480253 (diff) | |
NArith: implicit length argument for Bv2N
| -rw-r--r-- | CHANGES.md | 1 | ||||
| -rw-r--r-- | theories/NArith/Ndigits.v | 6 |
2 files changed, 5 insertions, 2 deletions
diff --git a/CHANGES.md b/CHANGES.md index 363513e4f7..21d9c41073 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -28,6 +28,7 @@ Standard Library - Added lemmas about monotonicity of `N.double` and `N.succ_double`, and about the upper bound of number represented by a vector. + Allowed implicit vector length argument in `Ndigits.Bv2N`. Changes from 8.8.2 to 8.9+beta1 =============================== diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 0f585baa4a..fb1cef1ddd 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -546,8 +546,10 @@ Fixpoint Bv2N (n:nat)(bv:Bvector n) : N := | Vector.cons _ true n bv => N.succ_double (Bv2N n bv) end. +Arguments Bv2N {n} bv, n bv. + Definition ByteV2N {n : nat} : ByteVector n -> N := - Bv2N (n * 8) ∘ to_Bvector. + Bv2N ∘ to_Bvector. Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n. Proof. @@ -584,7 +586,7 @@ destruct a ; compute ; split ; intros x ; now inversion x. Qed. Lemma Bv2N_upper_bound (n : nat) (bv : Bvector n) : - (Bv2N n bv < N.shiftl_nat 1 n)%N. + (Bv2N bv < N.shiftl_nat 1 n)%N. Proof with simpl; auto. induction bv... - constructor. |