Function VLDataOf 

pub open spec fn VLDataOf<Len, C>(c: C) -> NBytesOf<Len, C>

{ NBytesOf(core::marker::PhantomData, c) }

Convenience constructor for NBytesOf.