aboutsummaryrefslogtreecommitdiff
path: root/src/Util/NatUtil.v
Commit message (Expand)AuthorAge
* 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-06-29 04:56:15 +0000