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

Implement lifting between nested tuples and records #75

Closed tlringer closed 4 years ago

tlringer commented 4 years ago

This is a draft PR so that I can see all outstanding tasks left before merging.

tlringer commented 4 years ago

Document some goals after this: User-supplied equivalences, handling tuples nested differently, then back to UF stuff and eventually our fancy HoTT solver progress

tlringer commented 4 years ago

There's still more work after this to generalize further and to make this more configurable, but I'm OK with the current separation of concerns.