4 ms·
You 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.
by johncolanduoni 9y ago
You 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.