[isabelle-dev] is_concealed

[Florian Haftmann]

See now http://isabelle.in.tum.de/reports/Isabelle/rev/5f060de2dfd6

	Florian

On 20.11.2014 17:34, Dmitriy Traytel wrote:
> Sorry for reviving an ancient thread, but have the constants defined by
> inductive ever been visible to find_consts since Florian's commit (I
> presume 4a3747517552 ?).
> 
> Today in be4a911aca71 (but also in Isabelle2014 and even in
> Isabelle2012) in the following
> 
> inductive xyz :: bool where "xyz"
> find_consts name: xyz
> ML ‹Consts.is_concealed (Sign.consts_of @{theory}) @{const_name xyz}›
> 
> find_consts says "found nothing" and Consts.is_concealed says true.
> 
> Visibility of constants is of course also important beyond find_consts,
> e.g. for auto-completion.
> 
> Dmitriy
> 
> On 09.09.2010 09:57, Florian Haftmann wrote:
>> Am 09.09.2010 09:15, schrieb Florian Haftmann:
>>> Am 09.09.2010 09:02, schrieb Tobias Nipkow:
>>>> Lars noticed an anomaly and Gerwin tracked it down:
>>>> Command find_consts searches only for `visible' constants. Those defined
>>>> by primrec and fun are visible, but those defined by inductive(_set) are
>>>> concealed. It seems that the latter should be visible, too, right? If
>>>> so, can somebody close to "inductive" fix that?
>> Pushed.
>>
>> 	Florian
>>
>>
>>
>> _______________________________________________
>> Isabelle-dev mailing list
>> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141127/b15ac1d5/attachment.sig>