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?
sections are not hopeless. Lemmas (and theorems etc.) do work well in sections, and Instances can be made global.
OTOH effects of notations, Ltac, and for some reason (???)
Typeclasses Opaque don’t extend beyond sections.
if you rely on setoid rewriting, and declare Params instances, you’ll want those outside of sections (since those specify an argument count)
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