Zulip Chat Archive

Stream: new members

Topic: Coq for Lean users (or vice versa)?


view this post on Zulip Alexandre Rademaker (Nov 22 2019 at 01:51):

Does anyone know about any document comparing the two systems ? I am having hard time trying to understand the syntax of Coq and trying to figure out the equivalent one in Lean.

view this post on Zulip Simon Hudon (Nov 22 2019 at 03:31):

You should look at https://github.com/jldodds/coq-lean-cheatsheet

view this post on Zulip Kevin Buzzard (Nov 22 2019 at 07:03):

Purists would tell you that because they're different systems you can't necessarily deduce that a good set-up in one translates over to a good set-up in the other

view this post on Zulip Simon Hudon (Nov 22 2019 at 12:46):

That's true. There are commonalities but you have to learn the idioms of both to use them effectively.


Last updated: May 09 2021 at 19:11 UTC