aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* Add ListUtil.{take,drop}_whileGravatar Jason Gross2018-07-24
* Make Z.modinv run on wf proofsGravatar Jason Gross2018-07-18
* Handle Z.pow in push_Zmod tacticGravatar Jason Gross2018-07-17
* Handle Z.pow in {push,pull}_ZmodGravatar Jason Gross2018-07-17
* Add minor lemmas to utilGravatar Jason Gross2018-07-17
* Make Z.div_mod_to_quot_rem strongerGravatar Jason Gross2018-07-10
* Shuffle some ZUtil lemmas aroundGravatar Jason Gross2018-07-08
* Fix an infinite loop in Z.peel_leGravatar Jason Gross2018-07-06
* Add ZUtil, list lemmasGravatar Jason Gross2018-07-02
* Fix a notation issue in previous commitGravatar Jason Gross2018-07-02
* Add more ListUtil proofsGravatar Jason Gross2018-07-02
* Add some list lemmasGravatar Jason Gross2018-07-02
* Make all parameters implicitGravatar Jasper Hugunin2018-07-02
* Prefer relations of the form [eq ==> eq ==> ... ==> eq] in setoidsGravatar Jason Gross2018-07-01
* Add useful list lemmasGravatar Jason Gross2018-06-29
* Add ZUtil.SortingGravatar Jason Gross2018-06-29
* Revert "Add more schemes for prod"Gravatar Jason Gross2018-06-28
* Add more schemes for prodGravatar Jason Gross2018-06-28
* Try out stronger land, lor boundsGravatar Jason Gross2018-06-27
* Add is_tighter_than_bool lemmasGravatar Jason Gross2018-06-27
* Add lnot mod pull/push lemmasGravatar Jason Gross2018-06-27
* Add missing Z.lnot_0 hintsGravatar Jason Gross2018-06-27
* Add more Z const hintsGravatar Jason Gross2018-06-27
* Remove lneg in favor of lnot_modulo (lneg was wrong)Gravatar Jason Gross2018-06-27
* Add some Z.land, Z.lor hintsGravatar Jason Gross2018-06-27
* Add a couple of zrange lemmasGravatar Jason Gross2018-06-26
* Add specialize_all_ways, fix a proof in src/Compilers/Z/ArithmeticSimplifierI...Gravatar Jason Gross2018-06-26
* Add Z.bneg, Z.lnegGravatar Jason Gross2018-06-26
* Slightly better definitions of some ZUtil functionsGravatar Jason Gross2018-06-26
* Add list_beqGravatar Jason Gross2018-06-22
* Add Option.List.bind_listGravatar Jason Gross2018-06-21
* Add seq_add, seq_len_0Gravatar Jason Gross2018-06-19
* Add ShowLinesGravatar Jason Gross2018-06-17
* Reserve a notatoin for ;;Gravatar Jason Gross2018-06-16
* Add zrange equalityGravatar Jason Gross2018-06-15
* Add ErrorT monad, and Show classGravatar Jason Gross2018-06-15
* Add decimal_string_of_ZGravatar Jason Gross2018-06-15
* Add some lemmas and defs to ListUtil.FoldBoolGravatar Jason Gross2018-06-14
* Set universe polymorphism in CPSNotationsGravatar Jason Gross2018-06-14
* Add notations for cpsbind, cps_option_bindGravatar Jason Gross2018-06-14
* Actually use primitive projections in PrimitiveHListGravatar Jason Gross2018-06-13
* Minor refactoringGravatar Jason Gross2018-06-13
* Add PrimitiveHList, PrimitiveProdGravatar Jason Gross2018-06-13
* Move Option.List.map to OptionList.map to fix name clashes in TupleGravatar Jason Gross2018-06-04
* Add Option.List.mapGravatar Jason Gross2018-06-04
* Move cps notations into a scopeGravatar Jason Gross2018-06-01
* Add more bind reserved notationsGravatar Jason Gross2018-05-31
* Move function argument out of fixpoint of List.map2Gravatar Jason Gross2018-05-21
* Backtrack on moving a notation to Notations.v, to fix conflictGravatar Jason Gross2018-05-06
* Fix notations to not conflict with bbvGravatar Jason Gross2018-05-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 13:14:56 +0000