Record attributeValue := AVMake {
  (** The value of the attribute. *)
  avValue : string;
  (** Attribute values are valid. *)
  avValid : validName avValue
}.
