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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
