aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/LanguageWf.v
Commit message (Expand)AuthorAge
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09
* Add Wf_reifyGravatar Jason Gross2018-12-20
* Add Wf_APP, Interp_reifyGravatar Jason Gross2018-12-20
* add interp_related_gen_of_wfGravatar Jason Gross2018-12-12
* Generalize expr.interp_relatedGravatar Jason Gross2018-12-12
* Add eqv_iff_eq_of_funextGravatar Jason Gross2018-12-11
* Switch to a more precise version of interp_related for rewritesGravatar Jason Gross2018-12-07
* Restrict [ident.cast] a bit moreGravatar Jason Gross2018-11-05
* Refactor/generalize some pipeline definitions/proofsGravatar Jason Gross2018-10-30
* Remove duplicate abstractionGravatar Jasper Hugunin2018-10-29
* Add interp_reify_as_interpGravatar Jason Gross2018-10-24
* Add placeholder rewrite rules for rewriting after boundsGravatar Jason Gross2018-10-14
* Guarantee that casting always returns inrangeGravatar Jason Gross2018-10-12
* Parameterize rewriter proofs over cast-outside-of-range behaviorGravatar Jason Gross2018-10-11
* Add wf_from_flat_to_flatGravatar Jason Gross2018-09-12
* 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 more instances for type.relatedGravatar Jason Gross2018-08-16
* Add related_hetero_iff_app_curriedGravatar Jason Gross2018-08-10
* Add more interp lemmasGravatar Jason Gross2018-08-09
* Add Wf_of_Wf3Gravatar Jason Gross2018-08-08
* Add lemmas about type.and_for_each_lhs_of_arrowGravatar Jason Gross2018-08-07
* Add another GeneralizeVar pass to add support for using Wf3Gravatar Jason Gross2018-08-07
* Add gen_interp_ProperGravatar Jason Gross2018-08-06
* Add app_curried_Proper_gen as an instanceGravatar Jason Gross2018-08-06
* Add related_iff_app_curriedGravatar Jason Gross2018-08-06
* Generalize interp flat lemmasGravatar Jason Gross2018-08-06
* Generalize wf_interp_ProperGravatar Jason Gross2018-08-06
* Add wf for DefaultValueGravatar Jason Gross2018-08-03
* Make wf_safe_t a bit strongerGravatar Jason Gross2018-08-02
* Generalize type.eqv a bitGravatar Jason Gross2018-07-30
* Integrate Wf and Interp proofsGravatar Jason Gross2018-07-30
* More proofs about wf / interpGravatar Jason Gross2018-07-27
* Add wf about reify/reflect listGravatar Jason Gross2018-07-27
* Move rewrites to the correct tacticGravatar Jason Gross2018-07-26
* Shuffle transport lemmas around, add more inversionGravatar Jason Gross2018-07-26
* Improve wf tacticsGravatar Jason Gross2018-07-26
* Minor improvements to wf frameworkGravatar Jason Gross2018-07-26
* Move some tactics to their proper placeGravatar Jason Gross2018-07-26
* Add Wf lemmas about SubstVarGravatar Jason Gross2018-07-26
* Add basic wf proofsGravatar Jason Gross2018-07-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 07:11:20 +0000