Coq for Lean users (or vice versa)?

Stream: new members

[Alexandre Rademaker]

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]

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

[Kevin Buzzard]

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]

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