Stream: Coq users

Topic: Typeclass instances in sections?


view this post on Zulip Shea Levy (Oct 31 2020 at 01:20):

Is it expected that declaring an instance inside vs outside a section impacts resolution? I've been using sections to structure code and avoid repeated copies of parameters, but it seems they have some semantic implications as well?

view this post on Zulip Karl Palmskog (Oct 31 2020 at 01:55):

https://coq.inria.fr/distrib/current/refman/addendum/type-classes.html#contexts

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

sections are not hopeless. Lemmas (and theorems etc.) do work well in sections, and Instances can be made global.

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 03:05):

OTOH effects of notations, Ltac, and for some reason (???) Typeclasses Opaque don’t extend beyond sections.

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 03:06):

if you rely on setoid rewriting, and declare Params instances, you’ll want those outside of sections (since those specify an argument count)

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 03:07):

TLDR, I’ve basically stopped putting definitions or types in sections. Some people copy-paste notations/hints by hand after the section ends (good luck keeping those in sync)


Last updated: Jan 31 2023 at 14:03 UTC