Hi Dmitriy, thanks for figuring out. I am currently having a look at it…
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@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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
