Stream: Coq users

Topic: In section: declare a variable but no instance


view this post on Zulip Pierre Courtieu (Oct 13 2020 at 12:11):

Hi,
Is it possible to declare a variable in a section without declaring an instance?

Class Foo := {
  foo: Type;
 }.

Section Foo.
  Print Instances Foo.
  Variable F:Foo.
  Print Instances Foo. (* F:Foo*)

view this post on Zulip Gaëtan Gilbert (Oct 13 2020 at 12:15):

you can do Variable F : id Foo but not with type syntactically Foo AFAIK

view this post on Zulip Théo Zimmermann (Oct 13 2020 at 12:44):

See also https://github.com/coq/coq/issues/13068. Maybe you have an opinion on this issue @Pierre Courtieu.

view this post on Zulip Paolo Giarrusso (Oct 13 2020 at 13:13):

Can I ask about > And I would still like to hear why let definitions do not trigger instance declarations (this was @roglo's initial problem, so I would say this inconsistency does create confusion in practice).

view this post on Zulip Paolo Giarrusso (Oct 13 2020 at 13:16):

My naive first impression, as a Coq user, is that lots of code handling x : T in context (and relatives) needs special care to handle x : T := t in context, and that’s just forgotten often enough that you learn early on to distrust local definitions

view this post on Zulip Paolo Giarrusso (Oct 13 2020 at 13:18):

so isn’t that the “why”?

view this post on Zulip Paolo Giarrusso (Oct 13 2020 at 13:19):

(I got this impression as beginner so it might be wrong — but I couldn’t even guess what subst’s would do)


Last updated: Jan 29 2023 at 01:02 UTC