Comparison to Coq/Isabelle-HOL?

Stream: new members

[Chris M]

Is there a go-to resource that explains how Lean compares to CoQ or Isabelle-HOL? Something I'm interested in specifically as of this moment is the difference between inductive definitions in Lean versus Coq or Isabelle-HOL.

[Mario Carneiro]

There is https://github.com/jldodds/coq-lean-cheatsheet for a basic rundown of the differences of Lean coming from Coq. Isabelle is quite a bit more different, and I don't know a similar kind of cheatsheet would be appropriate, although you might find some vague equivalence in isar proofs and tactics

[Mario Carneiro]

Regarding differences in inductive types, they are mostly the same between Coq and Lean - there are some differences that are rather technical (match instead of rec, non-uniform parametric types, coinductive types)

[Mario Carneiro]

I'm not entirely sure about the extent of inductive types supported by isabelle. I think it is more permissive in some ways but less permissive (of necessity) around inductive dependent type families