[isabelle-dev] Notes on datatype_new list
Makarius
makarius at sketis.net
Mon May 26 12:05:22 CEST 2014
On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:
>> (3) A genuine name space problem: "list" is concealed, and thus cannot
>> be completed in semantic completion.
>
> I presume you are referring to the fact that
>
> @{const_name Cons} = "List.list.Cons"
> @{const_name hd} = "List.list.hd"
> @{const_name map} = "List.list.map"
> @{const_name rec_list} = "List.list.rec_list"
>
> where the "list" component is optional. This behavior is deliberate --
> this is what the old package did with all the constants it defined. In
> other words,
> The only novelty is that we followed the same idiom for the other
> constants introduced by the package, such as "hd" and "map".
(This is the easy part of this thread.)
I fully agree with this uniform additional qualification -- it is mainly
for internal robustness.
The observed here problem is different: the type constructor "list"
somehow ends up in the name space with a "concealed" flag. There might be
one or more Binding.conceal too many in the BNF sources.
I should probably issue some warning or special PIDE markup whenever a
plain name given in user space is resolved to some concealed entity.
Makarius
More information about the isabelle-dev
mailing list