Open adferguson opened 12 years ago
HFT.hs should become it's own data structure, possible packaged up as a separate project.
Or, a more radical approach would be to simply generate this code directly from the Coq proof script.
Haha. Not yet. We'll get there.
oops, I should have closed #49 instead.
HFT.hs should become it's own data structure, possible packaged up as a separate project.
Or, a more radical approach would be to simply generate this code directly from the Coq proof script.