Function asn1_start_exact 

pub open spec fn asn1_start_exact(tag: Tag) -> Asn1StartDomain

{ asn1_start_exact_uint(tag.class, tag.constructed, tag_num_to_uint(tag.number)) }