Stream: Coq users

Topic: ✔ How can I say that variables satisfy certain typeclass?


view this post on Zulip Li-yao (Oct 14 2022 at 09:06):

Are you using Variable outside of a section? Try inside a section.

view this post on Zulip Gaëtan Gilbert (Oct 14 2022 at 09:09):

outside a section use Axiom for A and B, and Declare Instance for A_Eq ad A_Co

view this post on Zulip walker (Oct 14 2022 at 09:19):

Gaëtan Gilbert said:

outside a section use Axiom for A and B, and Declare Instance for A_Eq ad A_Co

That feels strange, I always assumed that axiom is a footgun. does that mean that Vairbale is also equally dangerous ?

view this post on Zulip Li-yao (Oct 14 2022 at 09:24):

When used outside any section, Variable is the same as Axiom.

view this post on Zulip Li-yao (Oct 14 2022 at 09:26):

But you also get a warning about not using Variable that way because you probably don't mean it.

view this post on Zulip walker (Oct 14 2022 at 09:27):

I see. understood

view this post on Zulip Notification Bot (Oct 14 2022 at 09:27):

walker has marked this topic as resolved.

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

More idiomatic and concise ways include either:

Context `{Countable A}.

or

Context `{!EqDecision A, !Countable A}.

in sections; stdpp uses Context a lot

view this post on Zulip walker (Oct 14 2022 at 16:54):

1 extra question, what does the ! mean ?

view this post on Zulip Gaëtan Gilbert (Oct 14 2022 at 16:58):

it means do not create a fresh typeclass for any typeclass argument
so for EqDecision it does nothing, but for Countable without the ! it would add another EqDecision hypothesis and use that instead of the manually declared one
(! is a modifier for ` )

view this post on Zulip Gaëtan Gilbert (Oct 14 2022 at 16:59):

so

Context `{!EqDecision A, !Countable A}.

is equivalent to

Context `{Countable A}.

view this post on Zulip Paolo Giarrusso (Oct 14 2022 at 22:12):

And if you bind two typeclasses that "inherit" from e.g. EqDecision, you almost always want to use the ! form; I've never seen a case where binding multiple EqDecision instances is reasonable.


Last updated: Jan 27 2023 at 02:04 UTC