uwplse / pumpkin-pi

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

Revisit the positive example #88

Open tlringer opened 4 years ago

tlringer commented 4 years ago

Stopped on this because the world ended and the POPL deadline didn't change---revisit this example since it might help folks understand changes to non-isomorphic types stuffed into equivalences a bit better.