Function VLData 

pub open spec fn VLData<Len>() -> VariedLen<Len>

{ VariedLen(core::marker::PhantomData) }

Convenience constructor for VariedLen.