Function creusot_contracts::util::unwrap

source ยท 
pub fn unwrap<T>(op: Option<T>) -> T
Expand description

Returns the inner value of an Option, given that it is not None

logic

match op {
    Some(t) => t,
    None => unreachable(),
}

requires 

op != None

ensures 

Some(result) == op