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

Support universe polymorphism #54

Open tlringer opened 5 years ago

tlringer commented 5 years ago

Simon is interested in integrating this into EFF at some point. For better EFF integration, our tool needs to support universe polymorphism.