Don't wrap body in a closure unless we need to check postconditions
In current versions of contracts, annotating code using lifetime elision on mutable references will cause it to stop compiling. This is somewhat related to #11.
#[requires(i < s.len())] // ERROR
fn idx(s: &mut [u8], i: usize) -> &mut u8 {
&mut s[i]
}
This issue is hard (though not impossible) to solve when the user specifies a postcondition with ensures or invariant, but we can sidestep it entirely when only preconditions are needed.
Edited by Dylan MacKenzie