aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ListUtil.v
Commit message (Expand)AuthorAge
...
* 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
* Cleanup: mostly moving lemmas to Util files, some moving lemmas to more gener...Gravatar jadep2016-04-28
* Cleanup of GF25519Gravatar jadep2016-04-20
* moved lemmas from ModularBaseSystemProofs to various Util filesGravatar jadep2016-04-20
* Added lemmas to Util/ that are needed for testbit.Gravatar jadep2016-04-19
* Finish absolutizing importsGravatar Jason Gross2016-03-10
* fix letify to only insert a term onceGravatar Andres Erbsen2016-01-06
* reorganized lemmas; moved several to ListUtil and ZUtil.Gravatar Jade Philipoom2015-11-24
* Added base_succ precondition to BaseSystem to help prove carrying.Gravatar Jade Philipoom2015-11-19
* ModularBaseSystem: carry_rep has boring modular arithmetic proofsGravatar Andres Erbsen2015-11-17
* ModularBaseSystem.carry: implement, state lemmas, some progress on proofsGravatar Andres Erbsen2015-11-17
* BaseSystem: more boringGravatar Andres Erbsen2015-11-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-25 15:03:32 +0000