Re: [isabelle] Indexed Sum/Product Operator



Am 04/12/2012 20:58, schrieb Makarius:
> 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.)

I was not talking of the search facility itself (as Gerwin noted, we have a
number of nifty tools beside find_const) but how to invoke it without having to
type the command name. Command completion is already nice, but still crude.
Because the name can be nondescriptive and the parameters unclear. An example of
what I mean: Larry was not aware of the type-based search via find_consts.
Contrast this with the nice box that cmd-f gives you in many tools, eg jedit.

Tobias

> 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.