aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZUtil.v
Commit message (Expand)AuthorAge
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* Split off pull_Zmod, push_Zmod from ZUtilGravatar Jason Gross2017-05-13
* Split off more ZUtil thingsGravatar Jason Gross2017-05-13
* Split off more of ZUtilGravatar Jason Gross2017-05-13
* Split off more of ZUtilGravatar Jason Gross2017-05-13
* Split off ZUtil initial hint databasesGravatar Jason Gross2017-05-13
* Split off Proper ZUtil lemmasGravatar Jason Gross2017-05-12
* Remove dead code in ZUtil (shiftl_by)Gravatar Jason Gross2017-05-12
* Split off notation and defs in ZUtilGravatar Jason Gross2017-05-12
* Remove dead Ltac code from ZUtilGravatar Jason Gross2017-05-11
* Suppress a warning about unused intropatternsGravatar Jason Gross2017-05-11
* s/appcontext/context/Gravatar Jason Gross2017-05-11
* Add Z2Nat.inj_0 to zsimplify_constGravatar Jason Gross2017-04-24
* More zutil lemmasGravatar Jason Gross2017-04-24
* Add some zutil lemmasGravatar Jason Gross2017-04-24
* Add Z.lt_le_flip_Proper_flip_implGravatar Jason Gross2017-04-09
* Add Z.pow_nonneg to zarithGravatar Jason Gross2017-04-09
* Make replace_with_neg more powerfulGravatar Jason Gross2017-04-09
* Handle more things in Z.peel_leGravatar Jason Gross2017-04-09
* Add Z.peel_leGravatar Jason Gross2017-04-09
* Add Z.log2_up_le_mono to zarithGravatar Jason Gross2017-04-09
* Add Z.max_le_compat Z.min_le_compat to zarithGravatar Jason Gross2017-04-09
* Add lemmas about shift bounds to ZUtilGravatar Jason Gross2017-04-09
* Fix missing unfoldGravatar Jason Gross2017-04-09
* Add sub_le_flip_le_ProperGravatar Jason Gross2017-04-09
* Add Z.shift{l,r}_opp_lGravatar Jason Gross2017-04-08
* Add some le proper flip lemmasGravatar Jason Gross2017-04-08
* do not use VerdiTactics in files we plan to keepGravatar Andres Erbsen2017-04-06
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* Add Z.log2_up_le_pow2_fullGravatar Jason Gross2017-03-31
* Add Z.one_succ Z.two_succ to zsimplify_const dbGravatar Jason Gross2017-03-28
* Add lemmas needed for saturated arithmetic [compact]Gravatar jadep2017-03-24
* Split off extra power of ltb_to_lt, split_andbGravatar Jason Gross2017-03-21
* Remove a line I forgot to remove in the previous commitGravatar Jason Gross2017-03-21
* Split off the extra power of rewrite_mod_small into rewrite_mod_mod_smallGravatar Jason Gross2017-03-21
* Make Z.rewrite_mod_small a bit more powerfulGravatar Jason Gross2017-03-21
* Make Z.ltb_to_lt a bit strongerGravatar Jason Gross2017-03-21
* Add invert_Some; add nat_N_Z to push_Zof_NGravatar Jason Gross2017-02-23
* move some lemmas from Ed25519 to ZUtilGravatar jadep2017-02-22
* Merge new base system (#112)Gravatar jadephilipoom2017-02-22
* Add ZUtil lemmasGravatar Jason Gross2017-02-06
* Move things from WordUtil to ZUtil, add word lemmaGravatar Jason Gross2017-02-06
* More zutilGravatar Jason Gross2017-02-03
* Add lemmas about bounds of Z.lor, and add Z.max_log2_upGravatar Jason Gross2017-02-03
* Add lemmas for Z ops ProperGravatar Jason Gross2017-02-03
* Add log2_up_le_fullGravatar Jason Gross2017-02-03
* Add Z.log2_up_nonneg to zarithGravatar Jason Gross2017-02-03
* Add ZUtil lemma from zetabaseGravatar Jason Gross2017-01-19
* Add Zmod_to_equiv_moduloGravatar Jason Gross2017-01-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 04:18:41 +0000