Closed yforster closed 3 years ago
When a proof is finally accepted by Coq it just means it is correct: the absence of mistakes mistake correct for readable or maintainable.
https://github.com/math-comp/mcb/blob/master/tex/chProofLanguage.tex#L1549
Thanks
When a proof is finally accepted by Coq it just means it is correct: the absence of mistakes mistake correct for readable or maintainable.
https://github.com/math-comp/mcb/blob/master/tex/chProofLanguage.tex#L1549