search

uwplse / pumpkin-pi

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
MIT License
49 stars 9 forks source link

Use sigma types instead #1

Closed tlringer closed 6 years ago

tlringer commented 6 years ago

This has better theoretical properties. If necessary, we can always refer to code before March 15th to extract the results from the sigma types when we want to.

Also, the code is still messy; this is before cleanup.