> Even the very title of the article doesn't make much sense: why would you _want_ to translate Z3 to Coq?
You misread both the title and the article itself. It's not about some sort of general translation from Z3 to Coq. It's about translating examples from a tutorial to compare certain introductory proofs and (for the SEND+MORE=MONEY) problem solving strategies.
You misread both the title and the article itself. It's not about some sort of general translation from Z3 to Coq. It's about translating examples from a tutorial to compare certain introductory proofs and (for the SEND+MORE=MONEY) problem solving strategies.