aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* Clean up notations after bbv removalHEADmasterBenjamin Barenblat2019-04-26
* Remove WordUtilBenjamin Barenblat2019-04-26
* Remove BoundedWordBenjamin Barenblat2019-04-26
* Add some move/transport eq lemmasJason Gross2019-04-22
* Add push_rew_fun_depJason Gross2019-04-22
* Add Primitive.reflect_eq_prodJason Gross2019-04-18
* Add some bool eqb lemmasJason Gross2019-04-05
* Don't eagerly unfold boolean functions, hopefully, in tc reflect searchJason Gross2019-04-05
* Hint reflect on negbJason Gross2019-04-05
* Add Z.combine_at_bitwidthJason Gross2019-04-02
* Add constr_fail and constr_fail_withJason Gross2019-03-31
* improve zero_bounds tacticjadep2019-03-26
* add some hints to the global databasesjadep2019-03-26
* Move some lemmas to appropriate placesjadep2019-03-25
* Add Forall2_Proper instancesJason Gross2019-03-08
* Add Forall2_map_map_iffJason Gross2019-03-08
* Fix issue with previous commitJason Gross2019-03-08
* Add some eq list_rect lemmas to ListUtilJason Gross2019-03-08
* Remove GlobalTacticalsJason Gross2019-03-08
* Fix grepeat tacticJason Gross2019-03-08
* Fix gprogress tacticalJason Gross2019-03-08
* Add some gtacticsJason Gross2019-03-08
* Add Forall2_forall_In_combine_iffJason Gross2019-03-07
* Add some eq lemmas to ListUtilJason Gross2019-03-07
* Add some Proper lemmas to ListUtilJason Gross2019-03-07
* Add reserved notations for \inJason Gross2019-03-05
* Add some minor reflect thingsJason Gross2019-03-04
* Make [reflect] a typeclass and add a bunch of lemmasJason Gross2019-03-04
* Add Option.{lift,map,combine}, List.Option.liftJason Gross2019-02-11
* Add zrange_rect{,_Proper,_Proper_dep}Jason Gross2019-02-02
* Add option_beq_heteroJason Gross2019-02-02
* Add remove_duplicatesJason Gross2019-01-24
* Define String.replaceJason Gross2019-01-18
* Remove ? notationJason Gross2019-01-17
* Add some more basic ZRange lemmasJason Gross2019-01-15
* Move StringMap into Strings/Jason Gross2019-01-15
* Add StringMapJason Gross2019-01-15
* Add String_as_OTJason Gross2019-01-15
* Autocompute s and c in WBW MontgomeryJason Gross2019-01-14
* Move le_{add,sub}_1_* to ZUtil.LeJason Gross2018-12-25
* Add has_body tacticJason Gross2018-12-21
* prove [eval_conditional_sub]jadep2018-12-21
* Add ZRange.cc_m, ZRange.is_bounded_by_bool_cc_mJason Gross2018-12-11
* Add ZRange.is_bounded_by_bool_normalize_constantJason Gross2018-12-11
* Add ZRange.normalize_constantJason Gross2018-12-11
* Add ZRange.is_bounded_by_bool_constantJason Gross2018-12-11
* Add ZRange.OperationBoundsJason Gross2018-12-11
* Add In_elements_mem_iffJason Gross2018-12-11
* Add Forall2_update_nthJason Gross2018-12-06
* Fix broken proofsJason Gross2018-12-04