Record attributeName := ANMake {
  (** The name of the attribute. *)
  anName  : string;
  (** Attribute names are valid. *)
  anValid : validName anName
}.
