The Coq mailing list

[Gregory Malecha <gregory AT bedrocksystems.com>]

Usually this works, if it doesn't, I often make a local notation that includes the parameter.

On Mon, Jan 6, 2020 at 6:34 PM Vadim Zaliva <vzaliva AT cmu.edu> wrote:

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

--

gregory malecha

gregory AT bedrocksystems.com

director of formal methods