aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZUtil
Commit message (Expand)AuthorAge
* Add Z.combine_at_bitwidthGravatar Jason Gross2019-04-02
* improve zero_bounds tacticGravatar jadep2019-03-26
* add some hints to the global databasesGravatar jadep2019-03-26
* Move some lemmas to appropriate placesGravatar jadep2019-03-25
* Move le_{add,sub}_1_* to ZUtil.LeGravatar Jason Gross2018-12-25
* Add ZRange.OperationBoundsGravatar Jason Gross2018-12-11
* Fix and prove bounds for fancymachine operationsGravatar jadep2018-09-28
* Minor improvements to various ZUtil things; boundsGravatar Jason Gross2018-08-25
* Minor rshi tweaksGravatar Jason Gross2018-08-24
* Add some cc_m morphismsGravatar Jason Gross2018-08-24
* Add Z.rshi_correct_fullGravatar Jason Gross2018-08-24
* Add Z.cc_m_eq_fullGravatar Jason Gross2018-08-24
* Add a few more zsimplify_const lemmas about shiftGravatar Jason Gross2018-08-24
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Add more zutil morphismsGravatar Jason Gross2018-08-13
* Add some Z.le Proper hints to zarithGravatar Jason Gross2018-08-13
* Fix split_bounds, prove it correctGravatar Jason Gross2018-08-13
* Make Z.modinv run on wf proofsGravatar Jason Gross2018-07-18
* Handle Z.pow in push_Zmod tacticGravatar Jason Gross2018-07-17
* Handle Z.pow in {push,pull}_ZmodGravatar Jason Gross2018-07-17
* Make Z.div_mod_to_quot_rem strongerGravatar Jason Gross2018-07-10
* Shuffle some ZUtil lemmas aroundGravatar Jason Gross2018-07-08
* Fix an infinite loop in Z.peel_leGravatar Jason Gross2018-07-06
* Add ZUtil, list lemmasGravatar Jason Gross2018-07-02
* Add ZUtil.SortingGravatar Jason Gross2018-06-29
* Add lnot mod pull/push lemmasGravatar Jason Gross2018-06-27
* Add missing Z.lnot_0 hintsGravatar Jason Gross2018-06-27
* Add more Z const hintsGravatar Jason Gross2018-06-27
* Remove lneg in favor of lnot_modulo (lneg was wrong)Gravatar Jason Gross2018-06-27
* Add some Z.land, Z.lor hintsGravatar Jason Gross2018-06-27
* Add Z.bneg, Z.lnegGravatar Jason Gross2018-06-26
* Slightly better definitions of some ZUtil functionsGravatar Jason Gross2018-06-26
* add instructions cc_m, rshi, and sub_with_get_borrow to pipeline in preparati...Gravatar Jade Philipoom2018-04-19
* add some lemmas aboud div and modGravatar Jade Philipoom2018-04-11
* Add new assembly-mimicking operations rshi, cc_m, and cc_lGravatar Jade Philipoom2018-04-11
* prove stronger bound on quotient error for barrett reductionGravatar Jade Philipoom2018-04-11
* move some lemmas to ZUtil/ListUtilGravatar Jade Philipoom2018-04-03
* Add Zdiv_0_l to zsimplify dbsGravatar Jason Gross2018-03-27
* move things from ZUtil.v into Div.vGravatar Jade Philipoom2018-02-23
* add three proofs to ZUtilGravatar Jade Philipoom2018-02-23
* add proof about Z.equiv_moduloGravatar Jade Philipoom2018-02-23
* create rewrite database for saturated operations on ZGravatar Jade Philipoom2018-02-23
* Add new modular addition operation on ZGravatar Jade Philipoom2018-02-23
* Split off ZRange lemmasGravatar Jason Gross2018-02-10
* Add a comment for why Z.peano_rect_strong exists.Gravatar David Benjamin2018-01-14
* Switch arithmetic to cps for Z * Z under the hoodGravatar Jason Gross2017-10-19
* Add mul_split_cps'Gravatar Jason Gross2017-10-19
* Update ZUtil cps definitionsGravatar Jason Gross2017-10-19
* Add ZUtil.CPSGravatar Jason Gross2017-10-19
* Add some ZUtil lemmasGravatar Jason Gross2017-10-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-17 15:15:45 +0000