Say I'm formalizing something in group theory, and I'm working with some action $\cdot$ of $(G, +)$ on a set. In my math textbook, the identity of $\cdot$ is explicitly mentioned once (if that), and then left implicit. In my formalization, do I have to constantly keep specifying $(G, \cdot)$, or can I temporarily set $\cdot$ as the default?
In my limited experience, mathematical writing uses "dynamic scope" like this a lot. Does this actually correspond to a computer scientist's definition of dynamic scope, and if so, do any proof assistants support this?
xassume its type is
t" (which is how people are interpreting your question). It would be helpful if you gave a specific example of what you'd like. Also, what you are looking for is not called dynamic scope. $\endgroup$