aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tuple.v
Commit message (Expand)AuthorAge
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Generalize Tuple.dec_fieldwiseGravatar Jason Gross2017-11-09
* More generalization of fieldwise'_Proper to dependent typesGravatar Jason Gross2017-11-09
* Generalize fieldwise Proper lemmasGravatar Jason Gross2017-11-09
* Add fieldwise_lift_andGravatar Jason Gross2017-11-09
* Add more versions of fieldwise_ProperGravatar Jason Gross2017-11-09
* Add fieldwise_ProperGravatar Jason Gross2017-11-09
* Add fieldwise_eq_iffGravatar Jason Gross2017-11-09
* Add fieldwise_map_from_list_iffGravatar Jason Gross2017-11-09
* Add Tuple.dec_eq{,'}Gravatar Jason Gross2017-11-07
* write and prove Tuple.map2_cpsGravatar jadep2017-06-25
* Add is_bounded_by_None_repeat_In_iffGravatar Jason Gross2017-06-20
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-29 20:28:11 +0000