idris-lang/Idris-dev — pull request #1174 by bmsherman (2014-05-02 11:23:03+00:00)
Title: Add laziness and some documentation

This pull request is in response to issue https://github.com/idris-lang/Idris-dev/issues/1121.

Most notably, there are changes to the type signatures and evaluation semantics for `(&&)`, `(||)`, `and`, and `or`. `(&&)` and `(||)` are now lazy in their second arguments, and may short-circuit. Correspondingly, `and` and `or` now take foldables which hold lazy `a`s. These functions also now use `foldl`, so that short-circuiting happens from left-to-right, which I view as consistent with the behavior of `(&&)` and `(||)`.

Data type eliminators (e.g., `maybe`, `either`, `list`) are now lazy in any arguments which are only executed conditionally, as well.