| Commit message (Expand) | Author | Age |
|---|
| ... | |
| * | Add a rudimentary arg parse module |  Jason Gross | 2018-08-30 |
| * | Do less reduction in split_in_context | Jason Gross | 2018-08-29 |
| * | Improve speed of do_with_exactly_one_hyp tactic | Jason Gross | 2018-08-29 |
| * | Add src/Util/PER.v | Jason Gross | 2018-08-29 |
| * | Add do_with_exactly_one_hyp | Jason Gross | 2018-08-29 |
| * | Minor improvements to various ZUtil things; bounds | Jason Gross | 2018-08-25 |
| * | Minor rshi tweaks | Jason Gross | 2018-08-24 |
| * | Add some cc_m morphisms | Jason Gross | 2018-08-24 |
| * | Add Z.rshi_correct_full | Jason Gross | 2018-08-24 |
| * | Add Z.cc_m_eq_full | Jason Gross | 2018-08-24 |
| * | Add some basic ZRange lemmas | Jason Gross | 2018-08-24 |
| * | Add ZRange.union_comm | Jason Gross | 2018-08-24 |
| * | Add a few more zsimplify_const lemmas about shift | Jason Gross | 2018-08-24 |
| * | Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtil | Jason Gross | 2018-08-23 |
| * | Fix bounds on n_corners_and_zero |  Jason Gross | 2018-08-16 |
| * | Prove monotonicity properties about zrange | Jason Gross | 2018-08-15 |
| * | Add more zutil morphisms | Jason Gross | 2018-08-13 |
| * | Fix some bounds analysis | Jason Gross | 2018-08-13 |
| * | Add some Z.le Proper hints to zarith | Jason Gross | 2018-08-13 |
| * | Fix previous commit | Jason Gross | 2018-08-13 |
| * | Move a lemma | Jason Gross | 2018-08-13 |
| * | Add the file proving split_bounds correct | Jason Gross | 2018-08-13 |
| * | Fix split_bounds, prove it correct | Jason Gross | 2018-08-13 |
| * | Factor through is_tighter_than_bool, add is_bounded_by_bool_Proper_if_sumbool... | Jason Gross | 2018-08-13 |
| * | Add some util lemmas | Jason Gross | 2018-08-13 |
| * | Add ListUtil.map_nth_default_seq | Jason Gross | 2018-08-10 |
| * | Make Prod.eta_expand also work in the context | Jason Gross | 2018-08-10 |
| * | Add ListUtil.{combine_repeat,combine_rev_rev_samelength} | Jason Gross | 2018-08-09 |
| * | Improve the power of split_andb | Jason Gross | 2018-08-09 |
| * | Reserve 'n notation in Notations.v | Jason Gross | 2018-08-08 |
| * | Add related_iff_app_curried | Jason Gross | 2018-08-06 |
| * | Generalize option_eq to support heterogenous relations | Jason Gross | 2018-08-02 |
| * | Add nth_error_combine | Jason Gross | 2018-08-01 |
| * | Fix some issues in previous commit | Jason Gross | 2018-07-30 |
| * | Add nat_rect_Proper_nondep_gen | Jason Gross | 2018-07-30 |
| * | Add more proper instances | Jason Gross | 2018-07-26 |
| * | Reserve ==, ===, ~= | Jason Gross | 2018-07-25 |
| * | Add option sequencing/return | Jason Gross | 2018-07-25 |
| * | Reserve ;;;, fix level of prefix # to not clash with infix # | Jason Gross | 2018-07-25 |
| * | Add ListUtil.{take,drop}_while | Jason Gross | 2018-07-24 |
| * | 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 |
| * | Add minor lemmas to util | 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 |
| * | Fix a notation issue in previous commit | Jason Gross | 2018-07-02 |
| * | Add more ListUtil proofs | Jason Gross | 2018-07-02 |
Jason Gross
Jason Gross