Haskell

Stream: new members

[edklencl]

it is me again,what is the difference between lean and haskell

[Martin Dvořák]

(1) Haskell writes :: for type and : for list construction. Lean writes : for type and :: for list construction.
(2) Haskell writes = for declaration and == for equality. Lean writes := for declaration and = for Prop-valued equality.
(3) Lean has dependent types, which Haskell doesn't.
(4) Haskell is for programming. Lean is for programming and theorem proving.

[Martin Dvořák]

[this comment is obsolete]

[Notification Bot]

This topic was moved here from #mathlib4 > Haskell by Eric Wieser.

[Arthur Paulino]

inductive constructors are namespaced in Lean 4. data constructors, in Haskell, aren't

In fact, namespacing in general can be considered a new feature wrt Haskell