Email Gateway (Aug 22 2022 at 19:55): Email Gateway (Aug 22 2022 at 19:55):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Dear list,
Is the following behavior standard?
val _ = Theory.setup((antiquotation_docitem @{binding docref}
DOF_core.default_cid) #>
(* deprecated syntax ^^^^^^*)
(antiquotation_docitem @{binding docitem_ref}
DOF_core.default_cid) #>
(* deprecated syntax ^^^^^^^^^^*)
(antiquotation_docitem @{binding docitem}
DOF_core.default_cid) #>
(docitem_antiquotation @{binding docref}
DOF_core.default_cid) #>
(* deprecated syntax ^^^^^^*)
(docitem_antiquotation @{binding docitem_ref}
DOF_core.default_cid) #>
(* deprecated syntax ^^^^^^^^^^*)
(docitem_antiquotation @{binding docitem}
DOF_core.default_cid) #>
ML_antiquotation_docitem_value @{binding
docitem_value})
Namely I have two different semantics for the same binding and Isabelle
does not complain about it!
Best wishes,
Yakoub.
Email Gateway (Aug 22 2022 at 19:56):From: Makarius <makarius@sketis.net>
Above only the name bindings are a standard feature of Isabelle;
antiquotation_docitem, docitem_antiquotation,
ML_antiquotation_docitem_value are defined in user space of your
application.
If these refer to different name spaces, there is no clash here. (Even
within the same name space, it is possible to override entries,
depending on the name space policy.)
I don't see anything non-standard here.
Makarius
Email Gateway (Aug 22 2022 at 19:57):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Thank you for the reply.
This mean that my application somehow break the default "name space policy".
Overriding entries would have been a standard behavior to me.
I think the effect f my application is worst!
Could you please point to an example or some guidelines related to the
configuration of "name space policy"? For a document model such as HOL?
I want that my application be a conservative extension of isar and my fear
is that I am using some function that supposed to be private and left
public.
Namely, I want to understand why I changed the "name space policy" in an
unintentional way.
Best wishes,
Yakoub.
Email Gateway (Aug 22 2022 at 19:57):From: Makarius <makarius@sketis.net>
A name binding is merely a description for a new name; it "reacts" with
a naming from the context to produce a new name space entry (full name
and name "accesses"). The key operations for this are Name_Space.declare
or Name_Space.define, which take a bool to say if you intend a "strict"
update. The normal situation is strict = true; there are rare examples
for strict = false, e.g. facts or cases in a proof body.
It is normal in Isabelle that the same name binding (and naming) can be
reused in different name spaces: e.g. a const "nat" and a type "nat",
both producing the same full name and name accesses in separate name spaces.
In the Prover IDE tells, the standard CTRL-hover idiom tells you about
internal full name and name space name (the "kind") for names referenced
in the source. Thus it is clear to the user what is intended.
My understanding of your example is that antiquotation_docitem etc. are
defined by yourself: updating different name spaces in the theory
context. This looks OK from the surface. It is still unclear to me what
the problem really is.
Makarius
Last updated: Apr 23 2024 at 08:19 UTC