| Commit message (Expand) | Author | Age |
|---|
| * | Make Z.modinv run on wf proofs |  Jason Gross | 2018-07-18 |
| * | Handle Z.pow in push_Zmod tactic | Jason Gross | 2018-07-17 |
| * | Handle Z.pow in {push,pull}_Zmod | Jason Gross | 2018-07-17 |
| * | Make Z.div_mod_to_quot_rem stronger |  Jason Gross | 2018-07-10 |
| * | Shuffle some ZUtil lemmas around | Jason Gross | 2018-07-08 |
| * | Fix an infinite loop in Z.peel_le | Jason Gross | 2018-07-06 |
| * | Add ZUtil, list lemmas | Jason Gross | 2018-07-02 |
| * | Add ZUtil.Sorting | Jason Gross | 2018-06-29 |
| * | Add lnot mod pull/push lemmas | Jason Gross | 2018-06-27 |
| * | Add missing Z.lnot_0 hints | Jason Gross | 2018-06-27 |
| * | Add more Z const hints | Jason Gross | 2018-06-27 |
| * | Remove lneg in favor of lnot_modulo (lneg was wrong) | Jason Gross | 2018-06-27 |
| * | Add some Z.land, Z.lor hints | Jason Gross | 2018-06-27 |
| * | Add Z.bneg, Z.lneg | Jason Gross | 2018-06-26 |
| * | Slightly better definitions of some ZUtil functions | Jason Gross | 2018-06-26 |
| * | add instructions cc_m, rshi, and sub_with_get_borrow to pipeline in preparati... |  Jade Philipoom | 2018-04-19 |
| * | add some lemmas aboud div and mod | Jade Philipoom | 2018-04-11 |
| * | Add new assembly-mimicking operations rshi, cc_m, and cc_l | Jade Philipoom | 2018-04-11 |
| * | prove stronger bound on quotient error for barrett reduction | Jade Philipoom | 2018-04-11 |
| * | move some lemmas to ZUtil/ListUtil | Jade Philipoom | 2018-04-03 |
| * | Add Zdiv_0_l to zsimplify dbs | Jason Gross | 2018-03-27 |
| * | move things from ZUtil.v into Div.v | Jade Philipoom | 2018-02-23 |
| * | add three proofs to ZUtil | Jade Philipoom | 2018-02-23 |
| * | add proof about Z.equiv_modulo | Jade Philipoom | 2018-02-23 |
| * | create rewrite database for saturated operations on Z | Jade Philipoom | 2018-02-23 |
| * | Add new modular addition operation on Z | Jade Philipoom | 2018-02-23 |
| * | Split off ZRange lemmas | Jason Gross | 2018-02-10 |
| * | Add a comment for why Z.peano_rect_strong exists. |  David Benjamin | 2018-01-14 |
| * | Switch arithmetic to cps for Z * Z under the hood | Jason Gross | 2017-10-19 |
| * | Add mul_split_cps' | Jason Gross | 2017-10-19 |
| * | Update ZUtil cps definitions | Jason Gross | 2017-10-19 |
| * | Add ZUtil.CPS | Jason Gross | 2017-10-19 |
| * | Add some ZUtil lemmas | Jason Gross | 2017-10-03 |
| * | More fine-grained tactics imports | Jason Gross | 2017-07-08 |
| * | More fine-grained imports | Jason Gross | 2017-07-08 |
| * | Add wrappers for subborrow and add_with_get_carry so they work when it is not... |  jadep | 2017-06-29 |
| * | Fix a typo in push_Zmod that was causing looping | Jason Gross | 2017-06-22 |
| * | Add ModInv | Jason Gross | 2017-06-18 |
| * | Stronger zero_bounds | Jason Gross | 2017-06-18 |
| * | Add div_nonneg to zarith | Jason Gross | 2017-06-18 |
| * | Add Z.div_nonneg | Jason Gross | 2017-06-18 |
| * | Unfold Z.mul_split_at_bitwidth for reification | Jason Gross | 2017-06-17 |
| * | Add ZUtil.Z2Nat | Jason Gross | 2017-06-15 |
| * | Add mul_split_at_bitwidth, define things in terms of that | Jason Gross | 2017-06-13 |
| * | Add Z.peano_rect_strong | Jason Gross | 2017-06-13 |
| * | Add Z.peano_rect | Jason Gross | 2017-06-13 |
| * | Add Z.mul_split | Jason Gross | 2017-06-13 |
| * | Add mod_pull_div{,_full} | Jason Gross | 2017-06-10 |
| * | More powerful replace_neg_with_pos | Jason Gross | 2017-06-10 |
| * | Fix a typo | Jason Gross | 2017-06-10 |
Jason Gross
Jason Gross
Jade Philipoom
David Benjamin
jadep