diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2022-02-18 16:49:08 +0100 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2022-02-18 16:49:08 +0100 |
commit | 965520037392fa6c523348e3ff9dff5b9d5c2313 (patch) | |
tree | bac4fe2ad596afb76cbbc164b07804624e31f9e6 /src/bva/BVList.v | |
parent | c13ff15571392b111ad0b335d10077ad7958d069 (diff) | |
download | smtcoq-965520037392fa6c523348e3ff9dff5b9d5c2313.tar.gz smtcoq-965520037392fa6c523348e3ff9dff5b9d5c2313.zip |
Remove deprecated and some warnings
Diffstat (limited to 'src/bva/BVList.v')
-rw-r--r-- | src/bva/BVList.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/bva/BVList.v b/src/bva/BVList.v index 025bbd2..4c28ece 100644 --- a/src/bva/BVList.v +++ b/src/bva/BVList.v @@ -589,7 +589,7 @@ Definition ult_list (x y: list bool) := (ult_list_big_endian (List.rev x) (List.rev y)). -Fixpoint slt_list_big_endian (x y: list bool) := +Definition slt_list_big_endian (x y: list bool) := match x, y with | nil, _ => false | _ , nil => false @@ -2103,7 +2103,7 @@ Proof. intro a. induction a as [ | xa xsa IHa ]. - intros. simpl. easy. - intros. - case b in *. simpl. rewrite IHa. simpl. omega. + case b in *. simpl. rewrite IHa. simpl. lia. simpl. case (k - 1 <? 0)%Z; simpl; now rewrite IHa. Qed. @@ -2117,8 +2117,8 @@ Lemma prop_mult_bool_step: forall k' a b res k, length (mult_bool_step a b res k k') = (length res)%nat. Proof. intro k'. induction k'. - - intros. simpl. rewrite prop_mult_bool_step_k_h_len. simpl. omega. - - intros. simpl. rewrite IHk'. rewrite prop_mult_bool_step_k_h_len. simpl; omega. + - intros. simpl. rewrite prop_mult_bool_step_k_h_len. simpl. lia. + - intros. simpl. rewrite IHk'. rewrite prop_mult_bool_step_k_h_len. simpl; lia. Qed. Lemma and_with_bool_len: forall a b, length (and_with_bool a (nth 0 b false)) = length a. |