aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/PartialEvaluationWithLetIn.v
Commit message (Expand)AuthorAge
* Backtrack on moving a notation to Notations.v, to fix conflictGravatar Jason Gross2018-05-06
* Fix notations to not conflict with bbvGravatar Jason Gross2018-05-06
* Don't use vm_compute with existentialsGravatar Jason Gross2018-05-05
* Update commentGravatar Jason Gross2018-05-05
* Fully finish flat_mapGravatar Jason Gross2018-05-05
* Fix flat_mapGravatar Jason Gross2018-05-05
* WIP on lists as cons cellsGravatar Jason Gross2018-05-05
* Remove vinterp_arrow functionGravatar Jason Gross2018-05-05
* Revert "WIP on inductive base_value"Gravatar Jason Gross2018-05-05
* WIP on inductive base_valueGravatar Jason Gross2018-05-05
* Revert "WIP with andres, not working pattern language"Gravatar Jason Gross2018-05-05
* WIP with andres, not working pattern languageGravatar Jason Gross2018-05-05
* Add comment about leaky abstractionGravatar Jason Gross2018-05-05
* Split off specialization to base types from specialization to identsGravatar Jason Gross2018-05-05
* Add type variables / substitutionsGravatar Jason Gross2018-05-05
* Change some notations for more readability by AndresGravatar Jason Gross2018-05-05
* Update cast -> annotateGravatar Jason Gross2018-05-05
* Parameterize over types and identifiersGravatar Jason Gross2018-05-05
* Add notesGravatar Jason Gross2018-05-05
* Add partial evaluationGravatar Jason Gross2018-05-05
* Some experiments with partial evaluation with letin without cpsGravatar Jason Gross2018-05-05