Implement better handling of opaque terms

uwplse / pumpkin-pi

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.

MIT License

49 stars 9 forks source link

Closed tlringer closed 3 years ago

tlringer commented 5 years ago

These just fail with a very cryptic error.

Either find a way around this, or implement better error handling for this case.