coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adam AT chlipala.net>
- To: Daniel Schepler <dschepler AT gmail.com>
- Cc: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Overriding default scoping
- Date: Sun, 06 Feb 2011 14:18:37 -0500
Daniel Schepler wrote:
Say I have a file which uses both the Ensembles and Reals libraries. Both
define a version of In: Ensembles.In is set membership, and RList.In is
membership of a real in an Rlist (a duplication of "list R"). As far as I can
tell, it seems to be random which version In will refer to. Is there any way
I could use a declaration like
Using Ensembles.In.
if Coq decides on using RList.In, to override that choice? I couldn't find
any
such thing looking through the reference manual (in particular I read through
section 2.6 "Libraries and qualified names").
The choice isn't random. It depends on the order in which you import the library modules, just like with 'open' in ML.
You might try [Import Ensembles.] to "bring its symbols to the foreground." That has the potential disadvantage of only working for whole modules, not individual identifiers. You always have the option of using commands like [Definition In := Ensembles.In.], where the new [In] is definitionally equal to the version you reference, though particular tactics may not always take advantage of that fact. Notations are another approach (overloadable via notation scopes) that is guaranteed to be invisible to tactics.
- [Coq-Club] Overriding default scoping, Daniel Schepler
- Re: [Coq-Club] Overriding default scoping, Adam Chlipala
Archive powered by MhonArc 2.6.16.