aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZUtil.v
Commit message (Expand)AuthorAge
* 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
* Add ZUtil lemmasGravatar Jason Gross2017-02-06
* Move things from WordUtil to ZUtil, add word lemmaGravatar Jason Gross2017-02-06
* More zutilGravatar Jason Gross2017-02-03
* Add lemmas about bounds of Z.lor, and add Z.max_log2_upGravatar Jason Gross2017-02-03
* Add lemmas for Z ops ProperGravatar Jason Gross2017-02-03
* Add log2_up_le_fullGravatar Jason Gross2017-02-03
* Add Z.log2_up_nonneg to zarithGravatar Jason Gross2017-02-03
* Add ZUtil lemma from zetabaseGravatar Jason Gross2017-01-19
* Add Zmod_to_equiv_moduloGravatar Jason Gross2017-01-09
* Fix precedence issue with 8.4Gravatar Jason Gross2016-11-08
* Prove things in ModularBaseSystemListZOperationsProofsGravatar Jason Gross2016-11-08
* Add log2_lt_pow2_altGravatar Jason Gross2016-11-08
* Work around bug 5189 (broken [Hint Resolve ->])Gravatar Jason Gross2016-11-08
* Add Z.lor_nonneg to zarithGravatar Jason Gross2016-11-08
* Z.ltb_to_lt now works in the goal, tooGravatar Jason Gross2016-11-05
* Add ZUtil.Z.log2_ones_lt_nonnegGravatar Jason Gross2016-11-02
* Add more ZUtilGravatar Jason Gross2016-11-02
* Add ZUtil lemmaGravatar Jason Gross2016-11-02
* Add ZUtil lemmaGravatar Jason Gross2016-11-02
* Add a ZUtil lemmaGravatar Jason Gross2016-11-02
* prove testbit_sub_pow2Gravatar Andres Erbsen2016-10-29
* Add some rewrites and admitted lemmasGravatar Jason Gross2016-10-27
* Add {push,pull}_Zof_N hint db to ZUtilGravatar Jason Gross2016-10-27
* prove admit about F.to_nat x mod mGravatar Andres Erbsen2016-10-27
* Add more simplify lemmas to ZUtilGravatar Jason Gross2016-10-17
* Add more simplify lemmas to ZUtilGravatar Jason Gross2016-10-17
* Add ZUtil lemmaGravatar Jason Gross2016-10-17
* Fix compatibility with sigT notationGravatar Jason Gross2016-10-10
* Make Ztestbit_fullGravatar Jason Gross2016-10-09
* Fix Ztestbit_full databaseGravatar Jason Gross2016-10-09
* Fix shiftr_spec_fullGravatar Jason Gross2016-10-09
* Add more to Ztestbit_fullGravatar Jason Gross2016-10-09
* Add a Ztestbit_full databaseGravatar Jason Gross2016-10-09
* Stronger Ztestbit, convert_to_ztestbitGravatar Jason Gross2016-10-07
* More zsimplify lemmas, stronger ZtestbitGravatar Jason Gross2016-10-07
* Weaken hyps of lor_range, add it to zarithGravatar Jason Gross2016-10-07
* Moved lemma to ZUtil and added an extra lemma jgross neededGravatar jadep2016-10-06
* Add testbit_add_shiftl_fullGravatar Jason Gross2016-10-06
* Use zutil_arith for side-conditions in testbitGravatar Jason Gross2016-10-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 18:39:15 +0000