Stream: Coq users

Topic: Export notation from section?

Joshua Grosso (Sep 11 2020 at 21:19):

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 Section?

Paolo Giarrusso (Sep 11 2020 at 21:19):

AFAIK no, but if you make one, let us know

Paolo Giarrusso (Sep 11 2020 at 21:20):

people have been known to try sacrificing goats for this purpose

Paolo Giarrusso (Sep 11 2020 at 21:20):

(never asked if that’s so hard to implement, but I assume it is)

Paolo Giarrusso (Sep 11 2020 at 21:21):

actually, now that I think about it... the assumption is that all variables are implicit, is it not?

Paolo Giarrusso (Sep 11 2020 at 22:35):

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.

Joshua Grosso (Sep 11 2020 at 23:56):

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.

Jasper Hugunin (Sep 12 2020 at 01:15):

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?)

Paolo Giarrusso (Sep 12 2020 at 09:16):

I try to close the section around the declaration needed for the notation, tho that does have its downsides.

Paolo Giarrusso (Sep 12 2020 at 09:16):

It's tolerable if the implicits are typeclasses

Last updated: Oct 13 2024 at 01:02 UTC