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

What kind of ornament relates unindexed to indexed Expr? #71

Open tlringer opened 5 years ago

tlringer commented 5 years ago

https://github.com/CoqHott/univalent_parametricity/blob/master/examples/Expr.v

tlringer commented 4 years ago

Could be something we can handle now with manual configuration