| Commit message (Expand) | Author | Age |
* | 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 |
* | Add some list lemmas | Jason Gross | 2018-07-02 |
* | Make all parameters implicit | Jasper Hugunin | 2018-07-02 |
* | Prefer relations of the form [eq ==> eq ==> ... ==> eq] in setoids | Jason Gross | 2018-07-01 |
* | Add useful list lemmas | Jason Gross | 2018-06-29 |
* | Add ZUtil.Sorting | Jason Gross | 2018-06-29 |
* | Revert "Add more schemes for prod" | Jason Gross | 2018-06-28 |
* | Add more schemes for prod | Jason Gross | 2018-06-28 |
* | Try out stronger land, lor bounds | Jason Gross | 2018-06-27 |
* | Add is_tighter_than_bool lemmas | Jason Gross | 2018-06-27 |
* | 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 a couple of zrange lemmas | Jason Gross | 2018-06-26 |
* | Add specialize_all_ways, fix a proof in src/Compilers/Z/ArithmeticSimplifierI... | Jason Gross | 2018-06-26 |
* | Add Z.bneg, Z.lneg | Jason Gross | 2018-06-26 |
* | Slightly better definitions of some ZUtil functions | Jason Gross | 2018-06-26 |
* | Add list_beq | Jason Gross | 2018-06-22 |
* | Add Option.List.bind_list | Jason Gross | 2018-06-21 |
* | Add seq_add, seq_len_0 | Jason Gross | 2018-06-19 |