Stream: Coq users

Topic: ✔ Different scopes with the same delimiting key


view this post on Zulip Ana de Almeida Borges (Mar 04 2022 at 13:29):

Is there anything that can be done about managing different scopes with the same key? For example, %Z is the delimiting key for both the stdlib integers and the mathcomp integers. I'm thinking something like %ZArith.Z to be more specific, although that of course does not work.

view this post on Zulip Pierre Roux (Mar 04 2022 at 13:39):

I don't think so, but one can always reasign keys. In validsdp, we have that for instance: https://github.com/validsdp/validsdp/blob/master/theories/cholesky_prog.v#L25

view this post on Zulip Ana de Almeida Borges (Mar 04 2022 at 13:41):

Cool, I didn't know that and it solves the problem, thanks!

view this post on Zulip Notification Bot (Mar 04 2022 at 13:41):

Ana de Almeida Borges has marked this topic as resolved.


Last updated: Jan 29 2023 at 01:02 UTC