Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] find_consts does not find constants from BNF p...

Email Gateway (Aug 22 2022 at 11:17):

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

I noticed that find_consts does not find the constants for the set and map functions and
the relator. For _ list, for example, none of the following commands find the functions
defined by the datatype declaration in List.thy (in Isabelle2015):

find_consts "(_ ⇒ _) ⇒ _ list ⇒ _ list" (* map not found *)
find_consts "(_ ⇒ _ ⇒ bool) ⇒ _ list ⇒ _ list ⇒ bool" (* list_all2 not found *)
find_consts "_ list ⇒ _ set" (* set not found *)

Could this be changed such that find_consts can find them? I was puzzled today in our
Isabelle course when I wanted to search for map and find_consts simply did not show it.

Best,
Andreas

Email Gateway (Aug 22 2022 at 11:18):

From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Andreas,

thanks for the report. (The BNF constants were concealed for almost two
years now, without anyone noticing!)

It should be better with the repository version isabelle/69a97fc33f7a.

Dmitriy

Email Gateway (Aug 22 2022 at 11:19):

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

I rarely use find_consts in my research work, but for teaching it is a great way to
explore what is already there in the library.

Thanks for changing it,
Andreas

Last updated: Nov 21 2024 at 12:39 UTC