Shea Levy (Oct 31 2020 at 01:20): 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?
Karl Palmskog (Oct 31 2020 at 01:55):https://coq.inria.fr/distrib/current/refman/addendum/type-classes.html#contexts
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.
Paolo Giarrusso (Oct 31 2020 at 03:05):OTOH effects of notations, Ltac, and for some reason (???) Typeclasses Opaque don’t extend beyond sections.
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)
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: Apr 19 2024 at 00:02 UTC