| Commit message (Expand) | Author | Age |
... | |
* | 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 |
* | Add ShowLines | Jason Gross | 2018-06-17 |
* | Reserve a notatoin for ;; | Jason Gross | 2018-06-16 |
* | Add zrange equality | Jason Gross | 2018-06-15 |
* | Add ErrorT monad, and Show class | Jason Gross | 2018-06-15 |
* | Add decimal_string_of_Z | Jason Gross | 2018-06-15 |
* | Add some lemmas and defs to ListUtil.FoldBool | Jason Gross | 2018-06-14 |
* | Set universe polymorphism in CPSNotations | Jason Gross | 2018-06-14 |
* | Add notations for cpsbind, cps_option_bind | Jason Gross | 2018-06-14 |
* | Actually use primitive projections in PrimitiveHList | Jason Gross | 2018-06-13 |
* | Minor refactoring | Jason Gross | 2018-06-13 |
* | Add PrimitiveHList, PrimitiveProd | Jason Gross | 2018-06-13 |
* | Move Option.List.map to OptionList.map to fix name clashes in Tuple | Jason Gross | 2018-06-04 |
* | Add Option.List.map | Jason Gross | 2018-06-04 |
* | Move cps notations into a scope | Jason Gross | 2018-06-01 |
* | Add more bind reserved notations | Jason Gross | 2018-05-31 |
* | Move function argument out of fixpoint of List.map2 | Jason Gross | 2018-05-21 |
* | Backtrack on moving a notation to Notations.v, to fix conflict | Jason Gross | 2018-05-06 |
* | Fix notations to not conflict with bbv | Jason Gross | 2018-05-06 |
* | More reserved notations | Jason Gross | 2018-05-06 |
* | Add another notation | Jason Gross | 2018-05-06 |
* | Fix a typo in last commit | Jason Gross | 2018-05-06 |
* | Add a reserved notation for #v | Jason Gross | 2018-05-06 |
* | Fix bounds analysis for saturated ops and remove unneeded comment | Jade Philipoom | 2018-04-30 |
* | Util.Loops: remove non-stdlib dependencies | Andres Erbsen | 2018-04-26 |
* | add instructions cc_m, rshi, and sub_with_get_borrow to pipeline in preparati... | Jade Philipoom | 2018-04-19 |
* | Fix a proof | Jason Gross | 2018-04-18 |
* | Change a proof in src/Util/Option | Jason Gross | 2018-04-18 |
* | Merge pull request #335 from mit-plv/cpsloops | Andres Erbsen | 2018-04-18 |
|\ |
|
* | | add a list lemma | Jade Philipoom | 2018-04-11 |
* | | 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 |
* | | Update number/string conversions | Jason Gross | 2018-04-09 |
* | | pass-through after Andres's review in #334 | Jade Philipoom | 2018-04-03 |
* | | move some lemmas to ZUtil/ListUtil | Jade Philipoom | 2018-04-03 |
* | | move some lemmas/hints to ListUtil | Jade Philipoom | 2018-04-03 |
* | | Add Zdiv_0_l to zsimplify dbs | Jason Gross | 2018-03-27 |
| * | move Loops from Experiments to Util | Andres Erbsen | 2018-03-27 |
| * | remove old loops code | Andres Erbsen | 2018-03-27 |
* | | Add list_case, a definition for match on list | Jason Gross | 2018-03-27 |
|/ |
|