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