aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZUtil.v
Commit message (Expand)AuthorAge
...
| * Add more hints in ZUtilGravatar Jason Gross2016-07-01
| * Add more ZUtil hintsGravatar Jason Gross2016-07-01
| * Add more hints to ZUtilGravatar Jason Gross2016-07-01
| * Add hint databases and a proof about Z.log2Gravatar Jason Gross2016-07-01
| * Add some proofs about Z.div and Z.mulGravatar Jason Gross2016-07-01
| * Fix a typo in Zsplit_sumsGravatar Jason Gross2016-07-01
| * Add tactic to split sums and differences in inequalitiesGravatar Jason Gross2016-07-01
| * Add fraction inequality reasoning tactics to ZUtilGravatar Jason Gross2016-07-01
| * Add a proof of 2 * x - x = xGravatar Jason Gross2016-06-30
| * Add a classification of n / m < 0Gravatar Jason Gross2016-06-30
| * Add a tactic for making use of destructed <? in ZGravatar Jason Gross2016-06-30
* | added and proved shift/or decode operation 'decode_bitwise'Gravatar jadep2016-06-30
| * Add pow_Zpow to Util.ZUtilGravatar Jason Gross2016-06-30
|/
* MergeGravatar jadep2016-06-14
|\
* | Finished admits for canonicalization proofs.Gravatar jadep2016-06-14
| * Fix for Coq 8.4pl2Gravatar Jason Gross2016-06-11
| * 8.5 fixesGravatar Jason Gross2016-06-10
|/
* First stage of canonicalization proofs complete; proved 3 carry loops reduce ...Gravatar jadep2016-05-20
* Cleanup: mostly moving lemmas to Util files, some moving lemmas to more gener...Gravatar jadep2016-04-28
* moved lemmas from ModularBaseSystemProofs to various Util filesGravatar jadep2016-04-20
* Added lemmas to Util/ that are needed for testbit.Gravatar jadep2016-04-19
* Finish absolutizing importsGravatar Jason Gross2016-03-10
* Factor out some bedrock dependencies into WordUtilGravatar Jason Gross2016-02-25
* a few lemmas in util about powers of 2 in Bedrock's various rewritten formsGravatar Jade Philipoom2016-02-15
* tweaks to util files, including automation for proving positivity/nonnegativi...Gravatar Jade Philipoom2016-02-15
* NumTheoryUtil : code cleanup; moved some lemmas to ZUtil.Gravatar Jade Philipoom2016-01-23
* Util: added util lemmas needed to instantiate EdDSA25519.Gravatar Jade Philipoom2016-01-05
* reorganized lemmas; moved several to ListUtil and ZUtil.Gravatar Jade Philipoom2015-11-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 20:07:27 +0000