aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Add PrimitiveSigmaGravatar Jason Gross2018-09-14
* Finish interp proof of abstract interpretationGravatar Jason Gross2018-09-14
* Add option_beq argumentsGravatar Jason Gross2018-09-13
* Add option_beqGravatar Jason Gross2018-09-13
* Remove unused RequireGravatar Vincent Laporte2018-09-12
* Solve two more zrange goalsGravatar Jason Gross2018-09-12
* Make a recording of what zrange proofs are leftGravatar Jason Gross2018-09-12
* Add wf_from_flat_to_flatGravatar Jason Gross2018-09-12
* Help for fixpoint refolding in expr.interpGravatar Jason Gross2018-09-11
* Improve documentation of binariesGravatar Jason Gross2018-09-11
* Add a rudimentary arg parse moduleGravatar Jason Gross2018-08-30
* Do less reduction in split_in_contextGravatar Jason Gross2018-08-29
* Improve speed of do_with_exactly_one_hyp tacticGravatar Jason Gross2018-08-29
* Add src/Util/PER.vGravatar Jason Gross2018-08-29
* Add do_with_exactly_one_hypGravatar Jason Gross2018-08-29
* Do almost all ZRange proofsGravatar Jason Gross2018-08-25
* Minor improvements to various ZUtil things; boundsGravatar Jason Gross2018-08-25
* Fix proofs broken by changes to cc_m proofsGravatar Jason Gross2018-08-24
* Minor rshi tweaksGravatar Jason Gross2018-08-24
* Add some cc_m morphismsGravatar Jason Gross2018-08-24
* Add Z.rshi_correct_fullGravatar Jason Gross2018-08-24
* Add Z.cc_m_eq_fullGravatar Jason Gross2018-08-24
* Add some basic ZRange lemmasGravatar Jason Gross2018-08-24
* Add ZRange.union_commGravatar Jason Gross2018-08-24
* Add a few more zsimplify_const lemmas about shiftGravatar Jason Gross2018-08-24
* Import prim token notations before using themGravatar Jason Gross2018-08-24
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Add more absint proofsGravatar Jason Gross2018-08-21
* Add more operation-specific proofsGravatar Jason Gross2018-08-21
* Do most of abs-int interp proofsGravatar Jason Gross2018-08-21
* Revert "Revert "Add more instances for type.related""Gravatar Jason Gross2018-08-20
* Revert "Add more instances for type.related"Gravatar Jason Gross2018-08-17
* Be more judicious about an instanceGravatar Jason Gross2018-08-17
* Add and_eqv_for_each_lhs_of_arrow_not_higher_orderGravatar Jason Gross2018-08-16
* Add andb_each_lhs_of_arrowGravatar Jason Gross2018-08-16
* Add more instances for type.relatedGravatar Jason Gross2018-08-16
* Fix bounds on n_corners_and_zeroGravatar Jason Gross2018-08-16
* Prove monotonicity properties about zrangeGravatar Jason Gross2018-08-15
* Fix another proof broken by wrong behavior of cbnGravatar Jason Gross2018-08-14
* Fix a proof broken by wrong behavior of cbnGravatar Jason Gross2018-08-14
* Add more zutil morphismsGravatar Jason Gross2018-08-13
* Fix some bounds analysisGravatar Jason Gross2018-08-13
* Add some Z.le Proper hints to zarithGravatar Jason Gross2018-08-13
* Fix previous commitGravatar Jason Gross2018-08-13
* Move a lemmaGravatar Jason Gross2018-08-13
* Fix a wrong bound computation (on negatives), fix a proofGravatar Jason Gross2018-08-13
* Add the file proving split_bounds correctGravatar Jason Gross2018-08-13
* Fix split_bounds, prove it correctGravatar Jason Gross2018-08-13
* Factor through is_tighter_than_bool, add is_bounded_by_bool_Proper_if_sumbool...Gravatar Jason Gross2018-08-13
* Add some util lemmasGravatar Jason Gross2018-08-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-27 22:41:09 +0000