Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
22
stars
20
forks
source link
Provide a convenience hypothesis with eqv assumptions in rewrite rules side-conditions #134
Closed
JasonGross closed 10 months ago
This should hopefully make https://github.com/mit-plv/fiat-crypto/pull/1778 easier