aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* Add decidable equality with nilGravatar Jason Gross2017-08-13
* Make some tactics a bit more powerfulGravatar Jason Gross2017-07-08
* More fine-grained tactics importsGravatar Jason Gross2017-07-08
* More fine-grained importsGravatar Jason Gross2017-07-08
* Add UnfoldArgGravatar Jason Gross2017-07-08
* prove an admit in ArithmeticSynthesisTestGravatar Andres Erbsen2017-07-06
* Add wrappers for subborrow and add_with_get_carry so they work when it is not...Gravatar jadep2017-06-29
* remove unused admit (has been moved to Tuple.v)Gravatar jadep2017-06-26
* Prove map2_appendGravatar Jason Gross2017-06-25
* write and prove Tuple.map2_cpsGravatar jadep2017-06-25
* Fix a typo in push_Zmod that was causing loopingGravatar Jason Gross2017-06-22
* Fix some minor naming bugs in sig_assoc tacticsGravatar Jason Gross2017-06-22
* src/Demo.v: a 200-line introduction to BaseSystem ideasGravatar Andres Erbsen2017-06-21
* Prove In_to_list_left_tl, In_left_hd, to_list_left_appendGravatar Jason Gross2017-06-21
* Add is_bounded_by_None_repeat_In_iff_ltGravatar Jason Gross2017-06-20
* Add fold_left_orb_true, fold_left_orb_pullGravatar Jason Gross2017-06-20
* Add is_bounded_by_None_repeat_In_iffGravatar Jason Gross2017-06-20
* [Require NatUtil] should not change [tauto]Gravatar Jason Gross2017-06-19
* Add ModInvGravatar Jason Gross2017-06-18
* Stronger zero_boundsGravatar Jason Gross2017-06-18
* Add div_nonneg to zarithGravatar Jason Gross2017-06-18
* Add Z.div_nonnegGravatar Jason Gross2017-06-18
* Add eq_ZToWordGravatar Jason Gross2017-06-17
* Unfold Z.mul_split_at_bitwidth for reificationGravatar Jason Gross2017-06-17
* finish tuple-ifying Montgomery APIGravatar jadep2017-06-16
* CPSify Saturated API in preparation for CPSifying Montgomery (see #194)Gravatar jadep2017-06-15
* Don't force [Require Import String] for debug msgsGravatar Jason Gross2017-06-15
* Fix a changed case in the proof in loop.vGravatar Jason Gross2017-06-15
* Better for_loop induction principleGravatar Jason Gross2017-06-15
* Export ZUtil.Z2Nat in ZUtilGravatar Jason Gross2017-06-15
* Add ZUtil.Z2NatGravatar Jason Gross2017-06-15
* Add for_cps_unroll1Gravatar Jason Gross2017-06-15
* Add eq_loop_cps_large_nGravatar Jason Gross2017-06-15
* move CPS notations to Util.CPSNotationsGravatar Andres Erbsen2017-06-15
* Loop changes, ScalarMultBase_correct with admitsGravatar Andres Erbsen2017-06-14
* loops WIPGravatar Andres Erbsen2017-06-14
* ScalarMult: Z -> G -> G (closes #193)Gravatar Andres Erbsen2017-06-14
* Add mul_split_at_bitwidth, define things in terms of thatGravatar Jason Gross2017-06-13
* Add Z.peano_rect_strongGravatar Jason Gross2017-06-13
* Add dec_eq_comparisonGravatar Jason Gross2017-06-13
* Add Z.peano_rectGravatar Jason Gross2017-06-13
* Add Z.mul_splitGravatar Jason Gross2017-06-13
* Fix zrange notation levelsGravatar Jason Gross2017-06-12
* Add unfold lemmas for id_with_altGravatar Jason Gross2017-06-11
* Add IdfunWithAltGravatar Jason Gross2017-06-11
* Add script to remake Tactics.v fileGravatar Jason Gross2017-06-11
* Add clearbody_allGravatar Jason Gross2017-06-11
* Fix loop notations, add for loopsGravatar Jason Gross2017-06-11
* Reserve some more notationsGravatar Jason Gross2017-06-11
* cps notations WIP...Gravatar Andres Erbsen2017-06-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 23:03:29 +0000