Login
From:
SYSTEMF @ EPFL
(Uncensored)
subscribe
Computing with opaque proofs – SYSTEMF @ EPFL
https://systemf.epfl.ch/blog/computing-with-opaque-proofs/
links
backlinks
Tagged with:
tutorials
coq
Roast topics
Find topics
Find it!
Computations with dependent types often get stuck on rewrites that use opaque lemmas. When the corresponding equality is decidable, these lemmas don't need to be made transparent to unblock computation.
