aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* Add HList.constGravatar Jason Gross2016-11-08
* Rename iffT, add some lemmas about tuple and hlistGravatar Jason Gross2016-11-08
* Add log2_lt_pow2_altGravatar Jason Gross2016-11-08
* Work around bug in 8.4Gravatar Jason Gross2016-11-08
* Work around bug 5189 (broken [Hint Resolve ->])Gravatar Jason Gross2016-11-08
* Add Z.lor_nonneg to zarithGravatar Jason Gross2016-11-08
* Add push_lift_optionGravatar Jason Gross2016-11-07
* Add map_is_mapt'Gravatar Jason Gross2016-11-07
* Add IffT, some Proper prod lemmasGravatar Jason Gross2016-11-07
* Add Proper prod instanceGravatar Jason Gross2016-11-07
* Add convoy_destructGravatar 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 HList lemmaGravatar 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
* Z.ltb_to_lt now works in the goal, tooGravatar Jason Gross2016-11-05
* Add reflect_iff_gen to Bool.vGravatar Jason Gross2016-11-05
* put EdDSA encoding sign bit at the MSBGravatar Andres Erbsen2016-11-04
* Fix divergence of Ltac match in 8.4Gravatar Jason Gross2016-11-02
* improve some fragile proofs (built on 8.4)Gravatar Andres Erbsen2016-11-02
* Add ZUtil.Z.log2_ones_lt_nonnegGravatar Jason Gross2016-11-02
* Add more ZUtilGravatar Jason Gross2016-11-02
* Add ZUtil lemmaGravatar Jason Gross2016-11-02
* Add ZUtil lemmaGravatar Jason Gross2016-11-02
* Add a ZUtil lemmaGravatar Jason Gross2016-11-02
* Change hlist implicit statusGravatar Jason Gross2016-11-01
* 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
* Add some interpretations things, speed up proofs in Ed25519Gravatar Jason Gross2016-10-31
* Fix for 8.5 build?Gravatar Jason Gross2016-10-30
* Add trueify to src/Util/PartiallyReifiedProp.vGravatar Jason Gross2016-10-30
* Add to_prop_and_reified_PropGravatar Jason Gross2016-10-30
* Add break_innermost_matchGravatar Jason Gross2016-10-30
* Fix a loop in PartiallyReifiedPropGravatar Jason Gross2016-10-30
* Add PartiallyReifiedPropGravatar Jason Gross2016-10-30
* prove Proper_SRepERepMulGravatar Andres Erbsen2016-10-29
* prove testbit_sub_pow2Gravatar Andres Erbsen2016-10-29
* Some work on proofs in src/Reflection/Z/Interpretations.vGravatar Jason Gross2016-10-27
* Add some rewrites and admitted lemmasGravatar Jason Gross2016-10-27
* Add beginnings of various interpretations of expression treesGravatar Jason Gross2016-10-27
* Add {push,pull}_Zof_N hint db to ZUtilGravatar Jason Gross2016-10-27
* prove admit about F.to_nat x mod mGravatar Andres Erbsen2016-10-27
* Fix implicit status of curryGravatar Jason Gross2016-10-27
* Add curry and uncurry to tupleGravatar Jason Gross2016-10-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 04:01:39 +0000