Macro mirai_annotations::get_model_field

macro_rules! get_model_field {
    ($target:expr, $field_name:ident, $default_value:expr) => { ... };
}

Retrieves the value of the specified model field, or the given default value if the model field is not set. This function has no meaning outside of a verification condition and should not be used with checked or debug_checked conditions. For example: precondition!(get_model_field!(x, f) > 1).