Function vstd::tokens::option_value_le_option_token

source ·
pub open spec fn option_value_le_option_token<Value, Token: ValueToken<Value>>(
    opt_value: Option<Value>,
    opt_token: Option<Token>,
    instance_id: InstanceId
) -> bool
Expand description
{
    match opt_value {
        Some(val) => {
            opt_token.is_some() && opt_token.unwrap().value() == val
                && opt_token.unwrap().instance_id() == instance_id
        }
        None => true,
    }
}