5 ms·
One difference with Coq is that in Coq everything is constructive. A proof of a precondition is an object and has to be constructed in F* you could use classica
by Jaxan 9y ago
One difference with Coq is that in Coq everything is constructive. A proof of a precondition is an object and has to be constructed in F* you could use classical logic, things are proven by a solver.
(I might be wrong.)
- johncolanduoni 9y agoYou can add the law of excluded middle in Coq like you can in F*, but it would put you at odds with almost all Coq code.