Haskell when and unless

Stream: new members

[Steven Shaw]

Is there something like Haskell's when and unless in Lean?

[Marcus Rossel]

There's an example and explanation of unless in this section of Functional Programming in Lean.

[Steven Shaw]

Thanks! I'm reading that book, but I'm not quite up to that chapter yet :sweat_smile:! For when, the "single-branched if" is exactly what I needed. :pray:

[Kyle Miller]

(@Steven Shaw Just so you know a little about what these are: in Lean there's both syntax for general terms and syntax for statements in do notation. The unless and single-branched if are do notation statements only.)