Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | prove [eval_conditional_sub] | jadep | 2018-12-21 |
| | |||
* | Add Forall2_update_nth | Jason Gross | 2018-12-06 |
| | |||
* | Remove ListUtil.List.repeat | Jason Gross | 2018-12-04 |
| | | | | | We are no longer checking against Coq 8.5, and it's simpler to not have two versions of `List.repeat` floating around. | ||
* | Add map_repeat, map_const | Jason Gross | 2018-11-11 |
| | |||
* | Add some natutil and listutil lemmas | Jason Gross | 2018-10-10 |
| | |||
* | Add map_update_nth_ext | Jason Gross | 2018-10-09 |
| | |||
* | Add some util lemmas | Jason Gross | 2018-08-13 |
| | |||
* | Add ListUtil.map_nth_default_seq | Jason Gross | 2018-08-10 |
| | |||
* | Add ListUtil.{combine_repeat,combine_rev_rev_samelength} | Jason Gross | 2018-08-09 |
| | |||
* | Add nth_error_combine | Jason Gross | 2018-08-01 |
| | |||
* | Add more proper instances | Jason Gross | 2018-07-26 |
| | |||
* | Add ListUtil.{take,drop}_while | Jason Gross | 2018-07-24 |
| | |||
* | Add minor lemmas to util | Jason Gross | 2018-07-17 |
| | |||
* | 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 |
| | |||
* | Add useful list lemmas | Jason Gross | 2018-06-29 |
| | |||
* | Add list_beq | Jason Gross | 2018-06-22 |
| | |||
* | Add seq_add, seq_len_0 | Jason Gross | 2018-06-19 |
| | |||
* | Move function argument out of fixpoint of List.map2 | Jason Gross | 2018-05-21 |
| | | | | | This allows us to make use of nested fixpoints involving map2, because the function argument can be inlined for guard checking now. | ||
* | add a list lemma | Jade Philipoom | 2018-04-11 |
| | |||
* | 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 list_case, a definition for match on list | Jason Gross | 2018-03-27 |
| | |||
* | add two proofs about lists | Jade Philipoom | 2018-02-23 |
| | |||
* | Strip the pointed instance names off of the default value in list expansion | Jason Gross | 2018-02-18 |
| | | | | This is required for reification to work, it seems | ||
* | Add expand_lists tactic | Jason Gross | 2018-02-18 |
| | |||
* | Add expand_list_correct to ListUtil | Jason Gross | 2018-02-12 |
| | |||
* | Generalize Forall2_forall_iff | Jason Gross | 2017-11-09 |
| | |||
* | src/Demo.v: a 200-line introduction to BaseSystem ideas | Andres Erbsen | 2017-06-21 |
| | |||
* | Don't rely on autogenerated names | Jason Gross | 2017-06-05 |
| | | | | | | This fixes all of the private-names warnings emitted by compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus the ones in coqprime, which I didn't touch). | ||
* | s/appcontext/context/ | Jason Gross | 2017-05-11 |
| | | | | They mean the same thing since 8.5, and appcontext is deprecated. | ||
* | do not use VerdiTactics in files we plan to keep | Andres Erbsen | 2017-04-06 |
| | |||
* | Add [Proof using] to most proofs | Jason Gross | 2017-04-04 |
| | | | | | | | | This closes #146 and makes `make quick` faster. The changes were generated by adding [Global Set Suggest Proof Using.] to GlobalSettings.v, and then following [the instructions for a script I wrote](https://github.com/JasonGross/coq-tools#proof-using-helper). | ||
* | Add lemmas needed for saturated arithmetic [compact] | jadep | 2017-03-24 |
| | |||
* | 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 |
| | |||
* | Fix a name clash | Jason Gross | 2017-03-14 |
| | |||
* | Add firstn_skipn | Jason Gross | 2017-03-14 |
| | |||
* | Add skipn_skipn | Jason Gross | 2017-03-14 |
| | |||
* | added Positional wrappers for Associational operations, added correctness ↵ | jadep | 2017-02-27 |
| | | | | proof of | ||
* | prove admits in Util.Tuple | Andres Erbsen | 2016-11-11 |
| | |||
* | Add fold_right_andb_true_iff_fold_right_and_True | Jason Gross | 2016-10-19 |
| | |||
* | Add Tuple.map2 | Jason Gross | 2016-10-19 |
| | |||
* | Work around bug #5112 ([Arguments id /] broken) | Jason Gross | 2016-09-30 |
| | |||
* | Move side lemmas to appropriate files | jadep | 2016-09-17 |
| |