aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* 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
* Add more Forall2 lemmasGravatar Jason Gross2018-12-04
* Add more ListUtil Forall LemmasGravatar Jason Gross2018-12-04
* Add some ListUtil lemmas about Forall2Gravatar Jason Gross2018-12-04
* Remove ListUtil.List.repeatGravatar Jason Gross2018-12-04
* Revert "Add inversion_clear tactics"Gravatar Jason Gross2018-12-04
* Add inversion_clear tacticsGravatar Jason Gross2018-12-04
* Global Set Fast Name PrintingGravatar Jason Gross2018-11-27
* Add related_sigT_by_eq proper lemmasGravatar Jason Gross2018-11-19
* Add more reserved notationsGravatar Jason Gross2018-11-19
* Add related_sigT_by_eqGravatar Jason Gross2018-11-16
* Add map_repeat, map_constGravatar Jason Gross2018-11-11
* Add a variant of cps_id that pulls the continuation from the lhsGravatar Jason Gross2018-11-08
* Add some zrange lemmasGravatar Jason Gross2018-11-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 07:00:48 +0000