where clause

Stream: general

[Greg Shuflin]

In Haskell, when you're writing a complicated function that has multiple pieces of functionality, it's often useful to break out those pieces of functionality into several complicated functions introduced by a where clause. Lean doesn't seem to have this syntax, just let. Is this a principled and deliberate syntax decision, or did no one get around to implementing where clauses?

[Damiano Testa]

You mean something like this?

[Greg Shuflin]

oh so there is a where syntax

[Greg Shuflin]

just wasn't documented in a place I could find