Function unwrap

pub fn unwrap<T>(op: Option<T>) -> T

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