4 ms·
Yes, I know, I mentioned the extraction. My question was whether it can help detecting translation errors from the first step.
by user2342 2y ago
Yes, I know, I mentioned the extraction.
My question was whether it can help detecting translation errors from the first step.
- cccbbbaaa 2y agoI'm not sure which first step you are talking about. Typically, one would write the program directly in Coq and use the extracted code as-is.