aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/LanguageInversion.v
Commit message (Expand)AuthorAge
* Better transport lemmas in LanguageInversionGravatar Jason Gross2018-08-09
* Add reflect_list_cps_idGravatar Jason Gross2018-08-03
* Better rewrite_type_transport_correctGravatar Jason Gross2018-08-02
* More proofs about wf / interpGravatar Jason Gross2018-07-27
* Stronger inversionGravatar Jason Gross2018-07-27
* Shuffle transport lemmas around, add more inversionGravatar Jason Gross2018-07-26
* Minor improvements to wf frameworkGravatar Jason Gross2018-07-26
* Actually improve expr.invert_oneGravatar Jason Gross2018-07-26
* Try again to fix expr inversionGravatar Jason Gross2018-07-26
* Improve expr.invert_one (hopefully)Gravatar Jason Gross2018-07-26
* Add some inversion lemmas and tacticsGravatar Jason Gross2018-07-25