aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZUtil.v
Commit message (Expand)AuthorAge
* Add instances about congruence moduloGravatar Jason Gross2016-07-28
* Add Z.mod_mod to zsimplifyGravatar Jason Gross2016-07-28
* Move most notation level declarations into UtilGravatar Jason Gross2016-07-27
* Restore functionality of Z.simplify_fractions_leGravatar Jason Gross2016-07-27
* Make Z.pre_reorder_fractions / Z.simplify_fractions_le not loopGravatar Jason Gross2016-07-27
* Add another ZUtil lemmaGravatar Jason Gross2016-07-26
* Merge branch 'master' of github.com:mit-plv/fiat-cryptoGravatar jadep2016-07-25
|\
* | A couple new util lemmasGravatar jadep2016-07-25
| * More Zpow in ZUtilGravatar Jason Gross2016-07-22
| * More ZUtilGravatar Jason Gross2016-07-22
| * More ZUtil lemmasGravatar Jason Gross2016-07-22
| * Revert "Revert "Add more ZUtil automation""Gravatar Jason Gross2016-07-22
| * Make the library 20% faster: [auto with *] is evilGravatar Jason Gross2016-07-22
| * Revert "Add more ZUtil automation"Gravatar Jason Gross2016-07-22
| * Add more ZUtil automationGravatar Jason Gross2016-07-22
| * Generalize div_sub_small a bitGravatar Jason Gross2016-07-22
|/
* Add another lemma to zarithGravatar Jason Gross2016-07-21
* Add another ZUtil lemmaGravatar Jason Gross2016-07-21
* Another ZUtil lemmaGravatar Jason Gross2016-07-21
* Fix broken proofsGravatar Jason Gross2016-07-21
* Add more ZUtilGravatar Jason Gross2016-07-21
* More ZUtil helper lemmasGravatar Jason Gross2016-07-21
* Add more ZUtil lemmasGravatar Jason Gross2016-07-21
* Add ZUtil lemmasGravatar Jason Gross2016-07-21
* Add Z.lt_le_incl to zarithGravatar Jason Gross2016-07-20
* Remove stuff from PseudoMersenneBaseParamProofs.vGravatar Jason Gross2016-07-19
* Move some definitions to Pow2Base (#24)Gravatar Jason Gross2016-07-18
* mergeGravatar jadep2016-07-10
|\
| * Add Z.div_0_l to ZUtilGravatar Jason Gross2016-07-08
* | Added mod case to zero_boundsGravatar jadep2016-07-08
| * Add pow2_mod to ZUtilGravatar Jason Gross2016-07-07
|/
* Fix notations, add &Gravatar Jason Gross2016-07-06
* Add notations for Z.shift{r,l} to ZUtilGravatar Jason Gross2016-07-06
* fixed indentation for new lemmas in ZUtilGravatar jadep2016-07-06
* Merged changes, including new ZUtil conventions.Gravatar jadep2016-07-06
|\
* | Factored out some proofs that rely only on base being powers of two, and defi...Gravatar jadep2016-07-06
| * Indentation in ZUtilGravatar Jason Gross2016-07-02
| * Make ZUtil more uniformGravatar Jason Gross2016-07-02
| * Fix for 8.4 evarsGravatar Jason Gross2016-07-01
| * Add ZUtil hintsGravatar Jason Gross2016-07-01
| * Add more hints to ZUtilGravatar Jason Gross2016-07-01
| * Add more hints in ZUtilGravatar Jason Gross2016-07-01
| * Add more ZUtil hintsGravatar Jason Gross2016-07-01
| * Add more hints to ZUtilGravatar Jason Gross2016-07-01
| * Add hint databases and a proof about Z.log2Gravatar Jason Gross2016-07-01
| * Add some proofs about Z.div and Z.mulGravatar Jason Gross2016-07-01
| * Fix a typo in Zsplit_sumsGravatar Jason Gross2016-07-01
| * Add tactic to split sums and differences in inequalitiesGravatar Jason Gross2016-07-01
| * Add fraction inequality reasoning tactics to ZUtilGravatar Jason Gross2016-07-01
| * Add a proof of 2 * x - x = xGravatar Jason Gross2016-06-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-04 06:24:52 +0000