Re: [isabelle-dev] is_concealed
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@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
Re: [isabelle-dev] is_concealed
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
Re: [isabelle-dev] is_concealed
It had been a lapsus. Regression is under way.
Florian
On 26.11.2014 15:39, Florian Haftmann wrote:
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
___
isabelle-dev mailing list
isabelle-...@in.tum.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
# HG changeset patch
# Parent 8bcd656dec352f13b8c2241a3ac05b5485812864
do not conceal inductive predicate names properly, following 4a3747517552
diff -r 8bcd656dec35 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.MLWed Nov 26 15:35:28 2014 +0100
+++ b/src/HOL/Tools/inductive.MLWed Nov 26 15:43:50 2014 +0100
@@ -827,14 +827,15 @@
Binding.name (space_implode _ (map (Binding.name_of o fst)
cnames_syn))
else alt_name;
+val is_auxiliary = length cs = 2;
val ((rec_const, (_, fp_def)), lthy') = lthy
- | Local_Theory.conceal
+ | is_auxiliary ? Local_Theory.conceal
| Local_Theory.define
((rec_name, case cnames_syn of [(_, syn)] = syn | _ = NoSyn),
- ((Thm.def_binding rec_name, @{attributes [nitpick_unfold]}),
+ ((Binding.conceal (Thm.def_binding rec_name), @{attributes
[nitpick_unfold]}),
fold_rev lambda params
(Const (fp_name, (predT -- predT) -- predT) $ fp_fun)))
- || Local_Theory.restore_naming lthy;
+ || is_auxiliary ? Local_Theory.restore_naming lthy;
val fp_def' =
Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def])
(cterm_of (Proof_Context.theory_of lthy') (list_comb (rec_const,
params)));
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] is_concealed
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
[isabelle-dev] is_concealed
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? Tobias ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
