coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] A simple typeclass question

From: Larry Lee <llee454 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] A simple typeclass question
Date: Fri, 03 Jan 2020 11:40:19 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=llee454 AT gmail.com; spf=Pass smtp.mailfrom=llee454 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qv1-f47.google.com
Ironport-phdr: 9a23:akfsyx/mKFWwyf9uRHKM819IXTAuvvDOBiVQ1KB40+McTK2v8tzYMVDF4r011RmVBN6dsa4fwLuO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhGiTanf79/Ixu7oQrVu8UKnIBvNrs/xhzVr3VSZu9Y33loJVWdnxb94se/4ptu+DlOtvwi6sBNT7z0c7w3QrJEAjsmNXs15NDwuhnYUQSP/HocXX4InRdOHgPI8Qv1Xpb1siv9q+p9xCyXNtD4QLwoRTiv6bpgRRn1gykFKjE56nnahM9tgqxbvhyvqQBwzYnbb4+aL/d+YqHQcMkGSWdbQspcVSpMCZ68YYsVCOoBOP5VoY/nqFsUtxu/BRSnCuXxxTBWm3T72qk60+A/Hg7Y0wEtH90DvW/brNXwLqgSUOS1wLPUwjXEavNbwDHw45XLfBA5ufyAQ658fM7LxUQsFw7JlEucpZHhMj+P2ekAsXCX4utvWO61lmIrtQ58riKyysojiITFnJwZxkzC+C5k2og6P8e4R1R+YdO8EJtfqSWaN4xuT8MnWW5ouSI6xqQfuZ6lYSQG0ZonyhHdZvCdfIiI5RXjVOmVIThmnn5qZLW/hxOq/UihzO3zSNW03U5UoiZZltTArHMA2hzJ5sSZV/dw+l2t1DmN2gzL7+FLO0E0la7VK547xb4wk4IesUDHHiDohkr7g6+be0o/9+in7uToeLTmppuGO4BojQH+N7wimtajDuQgLggOQ2+b9Pyg273k5E31WalFjvkrkqbCq53aPsQapquhAwBPyIoj6hC/Dy2n0NsCh3UHIkhFK1q7iN3iPEiLK/TlB9++hU6tmXFl3aPoJLrkV7HENGLS2JPscP4p70pRxVZukfhQ4ptVDvcKJ/elCRy5j8DREhJsa1/8+O3gEtgojtpDC1LKObeQNebpiXHN5u8rJLPRNoocuTK4MuZ8ovCy0jk2nlgSeaTv1pwSOijhT6ZWZn6BaH+pue8vVGIDvw4wVuvv0QTQXjtaZnL0VKU5tGhiVNCWSLzbT4Xou4SvmT+hF8QPNG9DA1GIV3zvctfcVg==

Hi everyone,

I have two very simple questions. Given a class:

Class A := { f : ... }.

and an instance of the class:

Definition inst : A := {| f := ... |}.

Is it possible for me to declare that every reference, within a
section, to a field in A (such as f) should use inst?

Second, Is there a way to do this if the record, inst, and call to f
are all in different files and wrapped within sections within these
files?

Thanks,
- Larry

[Coq-Club] A simple typeclass question, Larry Lee, 01/03/2020
- Re: [Coq-Club] A simple typeclass question, Vadim Zaliva, 01/07/2020
  - Re: [Coq-Club] A simple typeclass question, Gregory Malecha, 01/10/2020