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

Lifting probably has a bug with dependent IB #31

Open tlringer opened 5 years ago

tlringer commented 5 years ago

The current implementation logic for getting the indices to pass to IB doesn't make much sense, so I assume there's a bug which will show up when we test lifting with dependent IB.