Login
From:
Thomas Letan’s website
(Uncensored)
subscribe
Implementing Strongly-Specified Functions with the Program Framework · ~lthms
https://soap.coffee/~lthms/posts/StronglySpecifiedFunctionsProgram.html
links
backlinks
Roast topics
Find topics
Find it!
Program is the heir of the refine tactic. It gives you a convenient way to embed proofs within functional programs that are supposed to fade away during code extraction.
