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*)
you can do Variable F : id Foo
but not with type syntactically Foo AFAIK
See also https://github.com/coq/coq/issues/13068. Maybe you have an opinion on this issue @Pierre Courtieu.
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).
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
so isn’t that the “why”?
(I got this impression as beginner so it might be wrong — but I couldn’t even guess what subst
’s would do)
Last updated: Oct 13 2024 at 01:02 UTC