aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* 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
* Finish and enable rule-specific rewriter wf proofsGravatar Jason Gross2018-08-13
* Finish rule-specific rewriter wf proofsGravatar Jason Gross2018-08-13
* Improvements in rewrite-rule-specific proofsGravatar Jason Gross2018-08-13
* Split up rewrite rules proofs into multiple filesGravatar Jason Gross2018-08-13
* Prove rewrite-rule-independent parts of rewrite WfGravatar Jason Gross2018-08-13
* Don't guarantee anything about casting outside of rangeGravatar Jason Gross2018-08-10
* Add related_hetero_iff_app_curriedGravatar Jason Gross2018-08-10
* Add ListUtil.map_nth_default_seqGravatar Jason Gross2018-08-10
* Make Prod.eta_expand also work in the contextGravatar Jason Gross2018-08-10
* Better transport lemmas in LanguageInversionGravatar Jason Gross2018-08-09
* Add ListUtil.{combine_repeat,combine_rev_rev_samelength}Gravatar Jason Gross2018-08-09
* Improve the power of split_andbGravatar Jason Gross2018-08-09
* Don't fuse annotationsGravatar Jason Gross2018-08-09
* Add more interp lemmasGravatar Jason Gross2018-08-09
* Push back admits in interp lemmasGravatar Jason Gross2018-08-08
* Add Wf_of_Wf3Gravatar Jason Gross2018-08-08
* Reserve 'n notation in Notations.vGravatar Jason Gross2018-08-08
* Add some partial interp proofs for abs-intGravatar Jason Gross2018-08-08
* Add lemmas about type.and_for_each_lhs_of_arrowGravatar Jason Gross2018-08-07
* Finish relax interp proofsGravatar Jason Gross2018-08-07
* Add another GeneralizeVar pass to add support for using Wf3Gravatar Jason Gross2018-08-07
* Fix an issue with the previous commitGravatar Jason Gross2018-08-07
* Add Proof using to arithmetic proofsGravatar Jason Gross2018-08-07
* Add type.related_hetero3Gravatar Jason Gross2018-08-06
* Start setting up abs-int interp proofsGravatar Jason Gross2018-08-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 12:47:15 +0000