coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A simple typeclass question

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] A simple typeclass question
Date: Mon, 6 Jan 2020 15:33:39 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vzaliva AT cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-il1-f175.google.com
Ironport-phdr: 9a23:7dUCCxApfW8a4UI8rcf4UyQJP3N1i/DPJgcQr6AfoPdwSPv+pcbcNUDSrc9gkEXOFd2Cra4d0KyM7vmrADRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfL1/IA+ooQjRq8UajpZuJroswRbVv3VEfPhby3l1LlyJhRb84cmw/J9n8ytOvv8q6tBNX6bncakmVLJUFDspPXw7683trhnDUBCA5mAAXWUMkxpHGBbK4RfnVZrsqCT6t+592C6HPc3qSL0/RDqv47t3RBLulSwKMSMy/mPKhcxqlK9UrxyhqB5/zYDaY4+bKeRwcb/GcNwAWWZMRNxcWzBdDo6+aYYEEuoPPfxfr4n4v1YBogGxChStBOPq1zRHhWX53ak70+Q/Cw7NwQstH8wPsXvOqNX1NbkSXvquwabUyDXDcula1ing54jVax0sp+yHU7x3ccrU00YvFgXFg02WqYP/OjOayP0BvHSc7+V6Se2vi3QrpB12ojiqwMonl4rHhpoNx1za6Sl0xJw5KN64RUJhfNKpEZpduzuHO4Z0Qs4vRXxjtjwgxb0co5G7eTAHyJQ5yB7bbPyKa42I7QjiVOaVODt4hXZldK+mixa87EStyO3xWtO70FZNqSpFnd3MuW4X2xPP7ciHT+Nx/kan2TmRywDe8v9ILVwwmKbBKJMswqQ8mocSvEnCBCP6hUf7ga+OekUh4Oeo6uDnYrv8pp+bMo95kh/+Pb4zlcy+BOQ0KAkPUHKf+eS9yr3s51b0QbtUgf0tjqnVqozVJcEGpqKjHQBaz5sj5w6lDzi6yNQYgWUHLFVddR2biIjpIkjCL+z8DfeimFuhiyxrxvDDPr35GJrBNHnDkLH7fbZ88UFQ0gQzzcoMr65TX7oGObf4XlL7nN3eFB4wdQKukMj9D9Ao6IoSWGfHMKadMb3b+QuW9OsrIveFTIQQpXDwJ+VztK2mtmMwhVJIJfrh5pAQcn3tRq06cXXcWmLlh5I6KUlPphA3Hb7hjUDEXDJONS7rAvAMowojAYfjNr/tA4CghLvbgnW+F5xSI2FCUxWCSCi1MYqDXPgIZWSZJcozymVVB4jkcJco0FSVjCG/zrNmKuTO/ShB6cD82cNpoebWiFc/+SEmVsk=

Larry,

You mean like this?

Class A := { f : nat}.

Section Foo.
  Local Instance inst : A := {| f := 3 |}.

  Definition bar := f.
End Foo.

—
Vadim Zaliva
CMU ECE Ph.D. candidate
Mobile/Signal/WhatsApp: +1(510)220-1060

On Fri, Jan 3, 2020 at 8:40 AM Larry Lee <llee454 AT gmail.com> wrote:

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