aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tuple.v
Commit message (Expand)AuthorAge
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* prove compact obeys div/mod ruleGravatar jadep2017-05-01
* added [lastn] for tuplesGravatar jadep2017-05-01
* Fix nth_default for the tip of v8.6Gravatar Jason Gross2017-04-28
* add nth_default on tupleGravatar jadep2017-04-28
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
* Add Tuple.map_ProperGravatar Jason Gross2017-04-03
* Coalesce Tuple.pointwise2 and Tuple.fieldwiseGravatar Jason Gross2017-04-02
* Add Tuple.etaGravatar Jason Gross2017-04-01
* added tuple [repeat]Gravatar jadep2017-03-30
* Get rid of list-based Tuple.mapGravatar Jason Gross2017-03-30
* Add Tuple.pointwise2, Tuple.map_fixGravatar Jason Gross2017-03-30
* change map_with to mapi_with, a version that handles the index explicitlyGravatar jadep2017-03-29
* Add lemmas needed for saturated arithmetic [compact]Gravatar jadep2017-03-24
* Add strip_eta_tuple lemmasGravatar Jason Gross2017-02-28
* Better tuple_eta argumentsGravatar Jason Gross2017-02-28
* Add eta_tuple functionsGravatar Jason Gross2017-02-28
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 02:39:32 +0000