Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] find_consts does not find inductive sets

view this post on Zulip Email Gateway (Aug 22 2022 at 11:17):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
See now 61908914d191 and c94c65f35d01.

Florian
signature.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 11:17):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Florian,

Thanks for addressing this.

Best,
Andreas

view this post on Zulip Email Gateway (Aug 22 2022 at 11:23):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,

I noticed that find_consts does not find constants defined with inductive_set. Here is a
minimal example (for Isabelle2015):

theory Scratch imports Main begin
inductive_set foo :: "nat set => bool set" for x where "a : foo x"
find_consts "nat set => bool set" (* returns nothing *)
find_consts "nat set => bool => bool" (* returns foop *)
end

I think this should be changed such that inductively defined sets can also be
found---unless someone can convince me that the current behaviour is desirable.

Best,
Andreas

Last updated: Nov 21 2024 at 12:39 UTC