The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Hello All,

Yes, this seems a good idea. The main problem with record fields is
that they end up in the
scope where the record is declared. To prevent naming collisions, I
tend to prefix every
field with the name of the record but that leads to long names.
Sometimes I prefix the fields
with a shorthand of the name of the record but that becomes a bit
cryptic. For instance

Record process_process_set_equivalence_data: Type
:= mk_process_process_set_equivalence_data
   {
      ppsd_sig: signature;
      ppsd_process1: process;
      ppsd_proc_impl1: process_implementation ppsd_sig ppsd_process1;
      ppsd_process2: process;
      ppsd_proc_impl2: process_implementation ppsd_sig ppsd_process2;
      ppsd_set: Set;
      ppsd_set_impl: set_implementation ppsd_sig ppsd_set;
      process_set_equivalence:
         process_state ppsd_process2 -> ppsd_set -> Prop
   }.

Record process_equivalence_data: Type
:= mk_process_equivalence_data
   {
      ped_sig: signature;
      ped_process1: process;
      ped_proc_impl1: process_implementation ped_sig ped_process1;
      ped_process2: process;
      ped_proc_impl2: process_implementation ped_sig ped_process2;
      ped_equivalence:
         process_state ped_process1 -> process_state ped_process2 -> Prop;
   }.

Kind Regards,
Chris