The reference manual says that "Notations disappear when a section is closed." Still, is there any (possibly undocumented) way to make a
Notation visible outside of a
AFAIK no, but if you make one, let us know
people have been known to try sacrificing goats for this purpose
(never asked if that’s so hard to implement, but I assume it is)
actually, now that I think about it... the assumption is that all variables are implicit, is it not?
I ask because if variables are explicit, that just can’t work for many notations — but the export could just fail. And even with implicits, I can see exporting notation from sections is significantly different — you can’t just bind new arguments, you need to elaborate the body from scratch.
Oh, that makes sense now that you mention it. (In my particular case, I had applied all the arguments in my Notation, so theoretically it could work anywhere, but now I see why Notation-exporting hasn't been implemented in the compiler.)
I wonder if maybe exporting a Notation could create a function that moves the implicit arguments to be final arguments (so you'd have something like
<custom notation explicitArgs ...> <implicitArgs ...> and so inside the section, it could be written as just
<custom notation a b c>)—but, I guess that wouldn't work if the explicit arguments are themselves dependent on the implicit arguments.
Notations can also be more complex than just applying a function to arguments, what with binders and recursive notations and so on. That makes knowing what to do with section variables even more complicated. The general recommendation I've seen is to just re-declare the notation outside of the section if you have a way to make sense of it after generalizing the section variables. (Or in the case that your notation doesn't depend on any section variables, maybe you can move it before the section?)
I try to close the section around the declaration needed for the notation, tho that does have its downsides.
It's tolerable if the implicits are typeclasses
Last updated: Sep 25 2023 at 12:01 UTC