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