aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZUtil.v
Commit message (Expand)AuthorAge
* 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
* Add Z.pow_le_mono_{r,l} to zarithGravatar Jason Gross2016-10-06
* Add a lemma to Ztestbit about large indicesGravatar Jason Gross2016-10-06
* More zsimplify lemmasGravatar Jason Gross2016-10-04
* Add Zplus_minus to zsimplifyGravatar Jason Gross2016-10-04
* Weaken hyps of zutil lemmaGravatar Jason Gross2016-10-04
* Add a variant of add_shift_modGravatar Jason Gross2016-10-04
* Add ZUtil lemmaGravatar Jason Gross2016-10-04
* Add ZUtil lemmaGravatar Jason Gross2016-10-04
* Add Zmult_lt_compat_r to zarithGravatar Jason Gross2016-10-04
* Prevent infinite loops by not dealing with 0 mod _Gravatar Jason Gross2016-10-04
* Handle 0 mod _ in push_ZmodGravatar Jason Gross2016-10-04
* Handle ?x mod ?x in push_ZmodGravatar Jason Gross2016-10-04
* Z.ltb_to_lt now also handles eqbGravatar Jason Gross2016-10-04
* Reorganization, moving of lemmas to correct files, and 8.4 compatibilityGravatar jadep2016-09-21
* More 8.4 compatibilityGravatar jadep2016-09-14
* Moved lemmas to ZUtilGravatar jadep2016-09-13
* Work around bug #5073 (lia)Gravatar Jason Gross2016-09-07
* More zarithGravatar Jason Gross2016-08-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 11:30:57 +0000