aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZUtil.v
Commit message (Expand)AuthorAge
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Make Z.div_mod_to_quot_rem strongerGravatar Jason Gross2018-07-10
* Shuffle some ZUtil lemmas aroundGravatar Jason Gross2018-07-08
* Don't use deprecated compat notations in ZUtilGravatar Jason Gross2018-03-07
* move things from ZUtil.v into Div.vGravatar Jade Philipoom2018-02-23
* add three proofs to ZUtilGravatar Jade Philipoom2018-02-23
* Add Zpow_sub_1_nat_powGravatar Jason Gross2017-11-03
* Unfold Z.mul_split_at_bitwidth for reificationGravatar Jason Gross2017-06-17
* Export ZUtil.Z2Nat in ZUtilGravatar Jason Gross2017-06-15
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* Split off pull_Zmod, push_Zmod from ZUtilGravatar Jason Gross2017-05-13
* Split off more ZUtil thingsGravatar Jason Gross2017-05-13
* Split off more of ZUtilGravatar Jason Gross2017-05-13
* Split off more of ZUtilGravatar Jason Gross2017-05-13
* Split off ZUtil initial hint databasesGravatar Jason Gross2017-05-13
* Split off Proper ZUtil lemmasGravatar Jason Gross2017-05-12
* Remove dead code in ZUtil (shiftl_by)Gravatar Jason Gross2017-05-12
* Split off notation and defs in ZUtilGravatar Jason Gross2017-05-12
* Remove dead Ltac code from ZUtilGravatar Jason Gross2017-05-11
* Suppress a warning about unused intropatternsGravatar Jason Gross2017-05-11
* s/appcontext/context/Gravatar Jason Gross2017-05-11
* Add Z2Nat.inj_0 to zsimplify_constGravatar Jason Gross2017-04-24
* More zutil lemmasGravatar Jason Gross2017-04-24
* Add some zutil lemmasGravatar Jason Gross2017-04-24
* Add Z.lt_le_flip_Proper_flip_implGravatar Jason Gross2017-04-09
* Add Z.pow_nonneg to zarithGravatar Jason Gross2017-04-09
* Make replace_with_neg more powerfulGravatar Jason Gross2017-04-09
* Handle more things in Z.peel_leGravatar Jason Gross2017-04-09
* Add Z.peel_leGravatar Jason Gross2017-04-09
* Add Z.log2_up_le_mono to zarithGravatar Jason Gross2017-04-09
* Add Z.max_le_compat Z.min_le_compat to zarithGravatar Jason Gross2017-04-09
* Add lemmas about shift bounds to ZUtilGravatar Jason Gross2017-04-09
* Fix missing unfoldGravatar Jason Gross2017-04-09
* Add sub_le_flip_le_ProperGravatar Jason Gross2017-04-09
* Add Z.shift{l,r}_opp_lGravatar Jason Gross2017-04-08
* Add some le proper flip lemmasGravatar Jason Gross2017-04-08
* do not use VerdiTactics in files we plan to keepGravatar Andres Erbsen2017-04-06
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* Add Z.log2_up_le_pow2_fullGravatar Jason Gross2017-03-31
* Add Z.one_succ Z.two_succ to zsimplify_const dbGravatar Jason Gross2017-03-28
* Add lemmas needed for saturated arithmetic [compact]Gravatar jadep2017-03-24
* Split off extra power of ltb_to_lt, split_andbGravatar Jason Gross2017-03-21
* Remove a line I forgot to remove in the previous commitGravatar Jason Gross2017-03-21
* Split off the extra power of rewrite_mod_small into rewrite_mod_mod_smallGravatar Jason Gross2017-03-21
* Make Z.rewrite_mod_small a bit more powerfulGravatar Jason Gross2017-03-21
* Make Z.ltb_to_lt a bit strongerGravatar Jason Gross2017-03-21
* Add invert_Some; add nat_N_Z to push_Zof_NGravatar Jason Gross2017-02-23
* move some lemmas from Ed25519 to ZUtilGravatar jadep2017-02-22
* Merge new base system (#112)Gravatar jadephilipoom2017-02-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-29 18:01:35 +0000