| Commit message (Expand) | Author | Age |
|---|
| * | Add ap_transport to Equality.v |  Jason Gross | 2017-04-02 |
| * | Coalesce Tuple.pointwise2 and Tuple.fieldwise | Jason Gross | 2017-04-02 |
| * | Fix definition of BoundedWord | Jason Gross | 2017-04-01 |
| * | Split off BoundedWord.v from IntegrationTest.v | Jason Gross | 2017-04-01 |
| * | Split out Tactics.SubstLet | Jason Gross | 2017-04-01 |
| * | Add Tuple.eta | Jason Gross | 2017-04-01 |
| * | Add Z.log2_up_le_pow2_full | Jason Gross | 2017-03-31 |
| * | Add is_tighter_than_bool to zrange | Jason Gross | 2017-03-31 |
| * | More compatibility for etransitivity | Jason Gross | 2017-03-31 |
| * | Add [change_with_curried] to Curry.v | Jason Gross | 2017-03-31 |
| * | Add [etransitivity y], [etransitivity_rev] tactics | Jason Gross | 2017-03-31 |
| * | Add wordToZ{_gen,}_range | Jason Gross | 2017-03-30 |
| * | added tuple [repeat] |  jadep | 2017-03-30 |
| * | Use r[_ ~> _] for range rather than b[_ ~> _] | Jason Gross | 2017-03-30 |
| * | Rename Bounds to ZRange, use Prop, not bool | Jason Gross | 2017-03-30 |
| * | Get rid of list-based Tuple.map | Jason Gross | 2017-03-30 |
| * | Add a file dedicated to the definition of Z bounds | Jason Gross | 2017-03-30 |
| * | Add Tuple.pointwise2, Tuple.map_fix | Jason Gross | 2017-03-30 |
| * | remove commented-out lemma and add CPS version of mapi_with | jadep | 2017-03-29 |
| * | change map_with to mapi_with, a version that handles the index explicitly | jadep | 2017-03-29 |
| * | Add Z.one_succ Z.two_succ to zsimplify_const db | Jason Gross | 2017-03-28 |
| * | Don't reserve '(max_bitwidth' | Jason Gross | 2017-03-28 |
| * | Add a notation for printing | Jason Gross | 2017-03-28 |
| * | Add lemmas needed for saturated arithmetic [compact] | jadep | 2017-03-24 |
| * | Split off extra power of ltb_to_lt, split_andb | Jason Gross | 2017-03-21 |
| * | Remove a line I forgot to remove in the previous commit | Jason Gross | 2017-03-21 |
| * | Split off the extra power of rewrite_mod_small into rewrite_mod_mod_small | Jason Gross | 2017-03-21 |
| * | Make Z.rewrite_mod_small a bit more powerful | Jason Gross | 2017-03-21 |
| * | Make Bool.split_andb a bit more powerful | Jason Gross | 2017-03-21 |
| * | Make Z.ltb_to_lt a bit stronger | Jason Gross | 2017-03-21 |
| * | Add {firstn,skipn}_seq | Jason Gross | 2017-03-19 |
| * | generalize In_firstn_skipn_split | Jason Gross | 2017-03-19 |
| * | Add In_firstn_skipn_split | Jason Gross | 2017-03-19 |
| * | Add firstn_firstn_min | Jason Gross | 2017-03-19 |
| * | Add dec_eq_positive | Jason Gross | 2017-03-17 |
| * | Fix a name clash | Jason Gross | 2017-03-14 |
| * | Add firstn_skipn | Jason Gross | 2017-03-14 |
| * | Add split_prod | Jason Gross | 2017-03-14 |
| * | Add skipn_skipn | Jason Gross | 2017-03-14 |
| * | Move find_if_eq to Decidable.v, use Decidable in Named | Jason Gross | 2017-03-14 |
| * | Add faster versions of destruct_head_* | Jason Gross | 2017-03-14 |
| * | address some code review comments |  Andres Erbsen | 2017-03-02 |
| * | split the algebra library; use fsatz more | Andres Erbsen | 2017-03-02 |
| * | Add η principles for sigma types | Jason Gross | 2017-03-01 |
| * | Add dlet_nd notation | Jason Gross | 2017-03-01 |
| * | Add strip_eta_tuple lemmas | Jason Gross | 2017-02-28 |
| * | Better tuple_eta arguments | Jason Gross | 2017-02-28 |
| * | Add eta_tuple functions | Jason Gross | 2017-02-28 |
| * | Added operation (including creating ) | jadep | 2017-02-27 |
| * | added Positional wrappers for Associational operations, added correctness pro... | jadep | 2017-02-27 |
Jason Gross
jadep
Andres Erbsen