aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tuple.v
Commit message (Expand)AuthorAge
* More fine-grained util tactic filesGravatar Jason Gross2017-01-17
* More universe fixesGravatar Jason Gross2017-01-15
* Fix an issue with universesGravatar Jason Gross2017-01-15
* Add tuple lemmasGravatar Jason Gross2016-11-22
* Add fieldwise_mapGravatar Jason Gross2016-11-17
* use @implicits in rewrite (8.4)Gravatar Andres Erbsen2016-11-11
* prove admits in Util.TupleGravatar Andres Erbsen2016-11-11
* Add Tuple and HList lemmasGravatar Jason Gross2016-11-10
* Fix bug in 8.4Gravatar Jason Gross2016-11-09
* Add assoc_rightGravatar Jason Gross2016-11-09
* Fix Tuple.map2_SGravatar Jason Gross2016-11-09
* Add Tuple.map2_SGravatar Jason Gross2016-11-08
* Add map2_map{,_fst,_snd}Gravatar Jason Gross2016-11-08
* Rename iffT, add some lemmas about tuple and hlistGravatar Jason Gross2016-11-08
* Work around bug in 8.4Gravatar Jason Gross2016-11-08
* Add push_lift_optionGravatar Jason Gross2016-11-07
* Add tuple hd and tlGravatar Jason Gross2016-11-07
* Add more admitted tuple lemmasGravatar Jason Gross2016-11-06
* Add more admitted tuple lemmasGravatar Jason Gross2016-11-06
* Add Tuple.map_map2 (admitted)Gravatar Jason Gross2016-11-06
* Add admitted lemma about tuple map, add hlist lemGravatar Jason Gross2016-11-06
* Add Tuple lift pushGravatar Jason Gross2016-11-06
* Add functions for [tuple (option _) _]Gravatar Jason Gross2016-11-06
* Move hlist to new fileGravatar Jason Gross2016-11-01
* Fix a typo in the previous commitGravatar Jason Gross2016-11-01
* Generalize hlistGravatar Jason Gross2016-11-01
* Add hlist to tupleGravatar Jason Gross2016-11-01
* Fix implicit status of curryGravatar Jason Gross2016-10-27
* Add curry and uncurry to tupleGravatar Jason Gross2016-10-27
* Fix for Coq 8.4Gravatar Jason Gross2016-10-24
* Add more relations about fieldwiseGravatar Jason Gross2016-10-24
* Add Tuple.map2Gravatar Jason Gross2016-10-19
* Ed25519: add basepoint and prove most EdDSA preconditionsGravatar Andres Erbsen2016-10-10
* Add Tuple.mapGravatar Jason Gross2016-09-29
* Move side lemmas to appropriate filesGravatar jadep2016-09-17
* Fully qualify [Require]sGravatar Jason Gross2016-09-08
* Defined an equality comparison for tuples that uses bool instead of Prop (lik...Gravatar jadep2016-08-31
* Add length lemmasGravatar Jason Gross2016-08-12
* Make the library 20% faster: [auto with *] is evilGravatar Jason Gross2016-07-22
* tuple: applying functions to tuples of arbitrary lengthGravatar Andres Erbsen2016-07-12
* Merge of fixedlength and masterGravatar jadep2016-07-11
|\
| * [congruence] is more powerful in 8.5 than in 8.4Gravatar Andres Erbsen2016-07-11
* | Util/Tuple: added a version of from_list that doesn't require a proof of leng...Gravatar jadep2016-07-08
| * Util/Tuple: added a version of from_list that doesn't require a proof of leng...Gravatar jadep2016-07-08
* | Tuple: lift functions from lists to tuplesGravatar Andres Erbsen2016-07-03
|/
* Tuple: from_list_to_listGravatar Andres Erbsen2016-06-28
* Add decidable instances for sumwise and fieldwiseGravatar Jason Gross2016-06-27
* Variosu 8.5 fixesGravatar Jason Gross2016-06-20
* tuple toolingGravatar Andres Erbsen2016-06-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 21:04:35 +0000