Re: [isabelle] Indexed Sum/Product Operator



On Tue, 4 Dec 2012, Tobias Nipkow wrote:

Sometimes these "aspects" are still missing or only approximative, but the coverage is increasing over time. So the need for separate diagnostic commands like find_consts is more and more diminished.

The interesting part of the functionality of find_consts is search by a given type (a bit like Hoogle, if you speak Haskell). How do you plan to replace that by tooltips and hyperlinks?

This is just a different category of application: search over a "mathematical" library, and really good solutions to that are still missing. (I am occasionally attending the MKM conference, where people are discussing that.)


In contrast, the application sketched in this thread, you have your formal (con)text where you presently work already.

In the past query tools like find_theorems were often re-used to explore the local proof context, but this can be done more directly. Similarly replacement of interactive diagnostics can be anticipated for print_cases, print_facts, "thm calculation", "thm this" etc.

"Big" IDEs for Java do such things routinely. That is conceptually not such a big deal, and no need to go back to TTY-style commands.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.