aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZUtil/ZSimplify
diff options
context:
space:
mode:
authorGravatar Jason Gross <jagro@google.com>2018-08-24 15:12:16 -0400
committerGravatar Jason Gross <jagro@google.com>2018-08-24 15:12:16 -0400
commit87ed4dfaee47cd0fe79083844380886618effd09 (patch)
tree8e98049224c30b87c75cf291f3e178333c4f3564 /src/Util/ZUtil/ZSimplify
parent07fc5710981118e78d9e23e78e98c13a000e8635 (diff)
Add a few more zsimplify_const lemmas about shift
Diffstat (limited to 'src/Util/ZUtil/ZSimplify')
-rw-r--r--src/Util/ZUtil/ZSimplify/Core.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ZUtil/ZSimplify/Core.v b/src/Util/ZUtil/ZSimplify/Core.v
index 958c44f74..c850ddef6 100644
--- a/src/Util/ZUtil/ZSimplify/Core.v
+++ b/src/Util/ZUtil/ZSimplify/Core.v
@@ -8,7 +8,7 @@ Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z
Hint Rewrite <- Z.opp_eq_mul_m1 Z.one_succ Z.two_succ : zsimplify.
Hint Rewrite <- Z.div_mod using zutil_arith : zsimplify.
Hint Rewrite (fun x y => proj2 (Z.eqb_neq x y)) using assumption : zsimplify.
-Hint Rewrite Z.mul_0_l Z.mul_0_r Z.mul_1_l Z.mul_1_r Z.add_0_l Z.add_0_r Z.sub_0_l Z.sub_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_0_l Zmod_0_r Zmod_1_r Z.opp_0 Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r : zsimplify_const.
+Hint Rewrite Z.mul_0_l Z.mul_0_r Z.mul_1_l Z.mul_1_r Z.add_0_l Z.add_0_r Z.sub_0_l Z.sub_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_0_l Zmod_0_r Zmod_1_r Z.opp_0 Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r Z.shiftr_0_r Z.shiftr_0_l Z.shiftl_0_r Z.shiftl_0_l : zsimplify_const.
Hint Rewrite <- Z.one_succ Z.two_succ : zsimplify_const.