How can I namespace definitions within a single file?

Using Coq
1 
Section test1.
  Local Definition x := 0.
End test1.

Section test2.
  Fail Local Definition x := 1.
End test2.

I am surprised that this indeed fails. What are the semantics of Local? (This is in Coq 8.11.0, if it matters.)

2

Local Definition is like Definition: it adds an identifier to the current namespace/module. It does not circumvent the limitation that identifiers must be unique in each namespace. The difference affects how that identifier can be used by whoever imports your module (it must always be fully qualified).

To define x locally to each section, and not make it visible outside, use Let. (See the manual, on sections.)

To export multiple identifiers named x, use Definition with modules instead of sections. It also works to use Local Definition but it might not do what you expect; “full qualification” is extremely verbose.

1 Like