Hi all,
I’m excited to release a plugin I’ve been working on with Nate Yazdani. The plugin is called DEVOID, and the code is here.
The basic idea of the plugin is to derive functions and proofs over indexed types like vectors from non-indexed versions of those types like lists. It can do this automatically for a certain class of types (when the index is determined by a fold over the new index, like the length of a list) without any extra user input. For example, you don’t have to supply the relation between lists and vectors; the tool finds it automatically.
This is a preliminary release of the tool, which has some glitches to iron out, but if you’re interested, take a look at the plugin and play with some of the examples. I’d love feedback, bug reports, external contributions, and so on.
Best,
Talia