aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* Decidable: add [Z] and [nat] inequalitiesGravatar Andres Erbsen2016-10-10
* Fix compatibility with sigT notationGravatar Jason Gross2016-10-10
* Make Ztestbit_fullGravatar Jason Gross2016-10-09
* Fix Ztestbit_full databaseGravatar Jason Gross2016-10-09
* Fix shiftr_spec_fullGravatar Jason Gross2016-10-09
* Add more to Ztestbit_fullGravatar Jason Gross2016-10-09
* Add a Ztestbit_full databaseGravatar Jason Gross2016-10-09
* Stronger Ztestbit, convert_to_ztestbitGravatar Jason Gross2016-10-07
* More zsimplify lemmas, stronger ZtestbitGravatar Jason Gross2016-10-07
* Add eta_expand to Prod.vGravatar Jason Gross2016-10-07
* Weaken hyps of lor_range, add it to zarithGravatar Jason Gross2016-10-07
* Moved lemma to ZUtil and added an extra lemma jgross neededGravatar jadep2016-10-06
* Add testbit_add_shiftl_fullGravatar Jason Gross2016-10-06
* Use zutil_arith for side-conditions in testbitGravatar Jason Gross2016-10-06
* Add Z.pow_le_mono_{r,l} to zarithGravatar Jason Gross2016-10-06
* Add a lemma to Ztestbit about large indicesGravatar Jason Gross2016-10-06
* More zsimplify lemmasGravatar Jason Gross2016-10-04
* Add Zplus_minus to zsimplifyGravatar Jason Gross2016-10-04
* Weaken hyps of zutil lemmaGravatar Jason Gross2016-10-04
* Add a variant of add_shift_modGravatar Jason Gross2016-10-04
* Add ZUtil lemmaGravatar Jason Gross2016-10-04
* Add ZUtil lemmaGravatar Jason Gross2016-10-04
* Add Zmult_lt_compat_r to zarithGravatar Jason Gross2016-10-04
* Prevent infinite loops by not dealing with 0 mod _Gravatar Jason Gross2016-10-04
* Handle 0 mod _ in push_ZmodGravatar Jason Gross2016-10-04
* Handle ?x mod ?x in push_ZmodGravatar Jason Gross2016-10-04
* Z.ltb_to_lt now also handles eqbGravatar Jason Gross2016-10-04
* Work around bug 5107 (broken return inference)Gravatar Jason Gross2016-10-03
* Work around bug #5112 ([Arguments id /] broken)Gravatar Jason Gross2016-09-30
* Add Tuple.mapGravatar Jason Gross2016-09-29
* Revert "Add a locked version of [let] with fewer reductions"Gravatar Jason Gross2016-09-22
* Revert "Fix LockedLet"Gravatar Jason Gross2016-09-22
* Fix a typoGravatar Jason Gross2016-09-22
* Add a form of Let_In that carries a proofGravatar Jason Gross2016-09-22
* alternative signing derivationGravatar Andres Erbsen2016-09-22
* Util.LetIn: fix proper instanceGravatar Andres Erbsen2016-09-22
* Fix LockedLetGravatar Jason Gross2016-09-22
* Add a locked version of [let] with fewer reductionsGravatar Jason Gross2016-09-22
* Reorganization, moving of lemmas to correct files, and 8.4 compatibilityGravatar jadep2016-09-21
* Change [Let ... in ...] to [dlet ... in ...] (#67)Gravatar Jason Gross2016-09-19
* Add dec eq for option, listGravatar Jason Gross2016-09-18
* Util.Notations: change Let to match slet\Gravatar Andres Erbsen2016-09-18
* Add reserved notation for Let, change #Gravatar Jason Gross2016-09-17
* Move side lemmas to appropriate filesGravatar jadep2016-09-17
* deduplicate Let_In into src/Util/LetIn.vGravatar Andres Erbsen2016-09-17
* Add λn reserved notationGravatar Jason Gross2016-09-16
* Fix for Coq 8.5Gravatar Jason Gross2016-09-16
* Add more prop_of_optionGravatar Jason Gross2016-09-16
* Derive EdDSA.verify from equational specificationGravatar Andres Erbsen2016-09-16
* IterAssocOp: parameters before argumentsGravatar Andres Erbsen2016-09-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 06:48:35 +0000