Zulip Chat Archive

Stream: new members

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


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.

Simon Hudon (Nov 22 2019 at 03:31):

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

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

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: Dec 20 2023 at 11:08 UTC