aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ListUtil.v
Commit message (Expand)AuthorAge
* prove admits in Util.TupleGravatar Andres Erbsen2016-11-11
* Add fold_right_andb_true_iff_fold_right_and_TrueGravatar Jason Gross2016-10-19
* Add Tuple.map2Gravatar Jason Gross2016-10-19
* Work around bug #5112 ([Arguments id /] broken)Gravatar Jason Gross2016-09-30
* Move side lemmas to appropriate filesGravatar jadep2016-09-17
* Add nth_error_In from 8.6Gravatar Jason Gross2016-09-05
* Added rewrite hints for two ListUtil lemmasGravatar jadep2016-08-24
* Fix a typoGravatar Jason Gross2016-08-24
* Add map_cons from Coq 8.6Gravatar Jason Gross2016-08-24
* ListUtil.v : new proofs about sum_firstn for lists with nonnegative elementsGravatar jadep2016-08-21
* More 8.4 compatGravatar Jason Gross2016-08-16
* Add some list util, and decode'_map_mulGravatar Jason Gross2016-08-16
* Add a ListUtil lemmaGravatar Jason Gross2016-08-16
* Fix definition of [repeat] to match with 8.6Gravatar Jason Gross2016-08-16
* Fix for Coq 8.4Gravatar Jason Gross2016-08-16
* Add length lemmasGravatar Jason Gross2016-08-12
* Add ext_limb_widths_upper_boundGravatar Jason Gross2016-08-10
* Add lemma in 8.6 std lib to ListUtil for 8.4Gravatar Jason Gross2016-08-08
* Add a ListUtil lemmaGravatar Jason Gross2016-08-08
* Make the library 20% faster: [auto with *] is evilGravatar Jason Gross2016-07-22
* Add a distr_length databaseGravatar Jason Gross2016-07-19
* Add a lemma about sum_firstnGravatar Jason Gross2016-07-18
* Add a ListUtil lemmaGravatar Jason Gross2016-07-18
* Fix for Coq 8.4 (missing lemmas)Gravatar Jason Gross2016-07-18
* Fix some typos in the previous commitGravatar Jason Gross2016-07-18
* Add some lemmas about nth_default in boundsGravatar Jason Gross2016-07-18
* Added lemmas to ZUtil and NatUtil (for Testbit)Gravatar jadep2016-07-18
* mergeGravatar jadep2016-07-10
|\
* | added proofs about addition chain exponentiation for later use in ModularBase...Gravatar jadep2016-07-10
| * Fix ListUtil for Coq 8.4Gravatar Jason Gross2016-07-10
| * Update ListUtilGravatar Jason Gross2016-07-08
| * Add useful tactics and util lemmasGravatar Jason Gross2016-07-08
| * Add a ListUtil lemmaGravatar Jason Gross2016-07-08
| * Add a ListUtil lemmaGravatar Jason Gross2016-07-08
| * Fix ListUtil for Coq 8.4Gravatar Jason Gross2016-07-08
| * Add update_nth out of boundsGravatar Jason Gross2016-07-07
| * Add hint db in ListUtilGravatar Jason Gross2016-07-07
| * More ListUtil factsGravatar Jason Gross2016-07-07
| * Slightly better arguments in ListUtilGravatar Jason Gross2016-07-07
| * Correct hintdb namesGravatar Jason Gross2016-07-07
| * Add more about firstn to listutilGravatar Jason Gross2016-07-07
| * Add more update_nth to ListUtilGravatar Jason Gross2016-07-07
| * Fix ListUtil for Coq 8.4Gravatar Jason Gross2016-07-07
|/
* Add [update_nth] to ListUtil, change [set_nth]Gravatar Jason Gross2016-07-06
* Fix for broken 8.5 build in ListUtilGravatar Jason Gross2016-07-06
* Factored out some proofs that rely only on base being powers of two, and defi...Gravatar jadep2016-07-06
* remove trailing whitespace from src/Gravatar Andres Erbsen2016-06-20
* Finished admits for canonicalization proofs.Gravatar jadep2016-06-14
* progress on second stage (conditional constant-time subtraction) of canonical...Gravatar jadep2016-06-13
* starting rewrite using different definition of mapGravatar jadep2016-06-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 05:49:38 +0000