aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* Clean up notations after bbv removalHEADmasterGravatar Benjamin Barenblat2019-04-26
* Remove WordUtilGravatar Benjamin Barenblat2019-04-26
* Remove BoundedWordGravatar Benjamin Barenblat2019-04-26
* Add some move/transport eq lemmasGravatar Jason Gross2019-04-22
* Add push_rew_fun_depGravatar Jason Gross2019-04-22
* Add Primitive.reflect_eq_prodGravatar Jason Gross2019-04-18
* Add some bool eqb lemmasGravatar Jason Gross2019-04-05
* Don't eagerly unfold boolean functions, hopefully, in tc reflect searchGravatar Jason Gross2019-04-05
* Hint reflect on negbGravatar Jason Gross2019-04-05
* Add Z.combine_at_bitwidthGravatar Jason Gross2019-04-02
* Add constr_fail and constr_fail_withGravatar Jason Gross2019-03-31
* improve zero_bounds tacticGravatar jadep2019-03-26
* add some hints to the global databasesGravatar jadep2019-03-26
* Move some lemmas to appropriate placesGravatar jadep2019-03-25
* Add Forall2_Proper instancesGravatar Jason Gross2019-03-08
* Add Forall2_map_map_iffGravatar Jason Gross2019-03-08
* Fix issue with previous commitGravatar Jason Gross2019-03-08
* Add some eq list_rect lemmas to ListUtilGravatar Jason Gross2019-03-08
* Remove GlobalTacticalsGravatar Jason Gross2019-03-08
* Fix grepeat tacticGravatar Jason Gross2019-03-08
* Fix gprogress tacticalGravatar Jason Gross2019-03-08
* Add some gtacticsGravatar Jason Gross2019-03-08
* Add Forall2_forall_In_combine_iffGravatar Jason Gross2019-03-07
* Add some eq lemmas to ListUtilGravatar Jason Gross2019-03-07
* Add some Proper lemmas to ListUtilGravatar Jason Gross2019-03-07
* Add reserved notations for \inGravatar Jason Gross2019-03-05
* Add some minor reflect thingsGravatar Jason Gross2019-03-04
* Make [reflect] a typeclass and add a bunch of lemmasGravatar Jason Gross2019-03-04
* Add Option.{lift,map,combine}, List.Option.liftGravatar Jason Gross2019-02-11
* Add zrange_rect{,_Proper,_Proper_dep}Gravatar Jason Gross2019-02-02
* Add option_beq_heteroGravatar Jason Gross2019-02-02
* Add remove_duplicatesGravatar Jason Gross2019-01-24
* Define String.replaceGravatar Jason Gross2019-01-18
* Remove ? notationGravatar Jason Gross2019-01-17
* Add some more basic ZRange lemmasGravatar Jason Gross2019-01-15
* Move StringMap into Strings/Gravatar Jason Gross2019-01-15
* Add StringMapGravatar Jason Gross2019-01-15
* Add String_as_OTGravatar Jason Gross2019-01-15
* Autocompute s and c in WBW MontgomeryGravatar Jason Gross2019-01-14
* Move le_{add,sub}_1_* to ZUtil.LeGravatar Jason Gross2018-12-25
* Add has_body tacticGravatar Jason Gross2018-12-21
* prove [eval_conditional_sub]Gravatar jadep2018-12-21
* Add ZRange.cc_m, ZRange.is_bounded_by_bool_cc_mGravatar Jason Gross2018-12-11
* Add ZRange.is_bounded_by_bool_normalize_constantGravatar Jason Gross2018-12-11
* Add ZRange.normalize_constantGravatar Jason Gross2018-12-11
* Add ZRange.is_bounded_by_bool_constantGravatar Jason Gross2018-12-11
* Add ZRange.OperationBoundsGravatar Jason Gross2018-12-11
* Add In_elements_mem_iffGravatar Jason Gross2018-12-11
* Add Forall2_update_nthGravatar Jason Gross2018-12-06
* Fix broken proofsGravatar Jason Gross2018-12-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-25 11:43:15 +0000