aboutsummaryrefslogtreecommitdiff
path: root/src/Util/NatUtil.v
Commit message (Expand)AuthorAge
* Add some natutil and listutil lemmasGravatar Jason Gross2018-10-10
* Fix some issues in previous commitGravatar Jason Gross2018-07-30
* Add nat_rect_Proper_nondep_genGravatar Jason Gross2018-07-30
* Add more proper instancesGravatar Jason Gross2018-07-26
* Add minor lemmas to utilGravatar Jason Gross2018-07-17
* [Require NatUtil] should not change [tauto]Gravatar Jason Gross2017-06-19
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* Add transparent equality proofs for fixed wordTGravatar Jason Gross2017-01-21
* Add nat_beq_to_eqGravatar Jason Gross2017-01-19
* Fix 8.4 build issueGravatar Jason Gross2016-10-23
* Prove an admitted NatUtil lemmaGravatar Jason Gross2016-10-23
* integrate bitwise operationsGravatar Andres Erbsen2016-10-12
* Equality for nat in natutilGravatar Jason Gross2016-09-16
* Add natutilGravatar Jason Gross2016-08-16
* Convert defined and mostly proven, modulo several admitted lemmas about Z ope...Gravatar jadep2016-08-09
* Fix 8.4 build.Gravatar jadep2016-07-25
* A couple new util lemmasGravatar jadep2016-07-25
* Add another lemma about +, <= to arithGravatar Jason Gross2016-07-20
* Fix for Coq 8.4 (omega used to be weaker)Gravatar Jason Gross2016-07-18
* Add more natsimplify le_dec lemmasGravatar Jason Gross2016-07-18
* Add more NatUtil lemmasGravatar Jason Gross2016-07-18
* Add natsimplify lemmas about eq_nat_decGravatar Jason Gross2016-07-18
* Added lemmas to ZUtil and NatUtil (for Testbit)Gravatar jadep2016-07-18
* Fix NatUtil for 8.4Gravatar Jason Gross2016-07-08
* Add useful tactics and util lemmasGravatar Jason Gross2016-07-08
* Add a NatUtil lemma and dbGravatar Jason Gross2016-07-08
* Fix ListUtil for Coq 8.4Gravatar Jason Gross2016-07-07
* Add [update_nth] to ListUtil, change [set_nth]Gravatar Jason Gross2016-07-06
* Prove that a ^ k <> 0Gravatar Jason Gross2016-06-30
* MergeGravatar jadep2016-06-14
|\
* | progress on second stage (conditional constant-time subtraction) of canonical...Gravatar jadep2016-06-13
| * 8.5 fixesGravatar Jason Gross2016-06-10
|/
* moved lemmas from ModularBaseSystemProofs to various Util filesGravatar jadep2016-04-20
* 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
* Util: added util lemmas needed to instantiate EdDSA25519.Gravatar Jade Philipoom2016-01-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-29 21:26:00 +0000