Function metadata_matches 

pub fn metadata_matches<T: ?Sized>(
    _value: T,
    _metadata: <T as Pointee>::Metadata,
) -> bool

Check that a value is compatible with some metadata.

If the value is a slice, this predicate asserts that the metadata equals the length of the slice, and that the total size of the slice is no more than isize::MAX. This latter property is assumed by pointer primitives such as slice::from_raw_parts.

• For T = [U], specializes to [metadata_matches_slice].
• For T = str, specializes to [metadata_matches_str].
• For T: Sized, specializes to true.

Why did we not make this a function fn metadata_of(value: T) -> <T as Pointee>::Metadata? Because this way is shorter: this corresponds to a single predicate in Why3 per type T. Defining a logic function that returns usize for slices is not so straightforward because almost every number wants to be Int. We would need to generate one abstract Why3 function metadata_of : T -> Metadata and an axiom view_usize (metadata_of value) = len (Slice.view value), so two Why3 declarations instead of one.

(open, inline)

dead