On Tue, May 20, 2014 at 12:09 PM, Kim-Ee Yeoh <ky3@atamo.com> wrote: It's briefly documented in the tutorial, see do notation: http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf Looks like the key bit is "will lift expr as high as possible within the current scope".