Hi Tjark,
Am 20.01.2013 um 22:21 schrieb Tjark Weber:
> On Fri, 2013-01-18 at 19:29 +0100, Jasmin Christian Blanchette wrote:
>> What's your concrete suggestion here?
>
> It's more of a curiosity than an issue, of course. Otherwise, I would
> suggest to: First, make sure that the behavior is not due to a bug or
> silly inefficiency in the metis code. Second, offer a way to suppress
> the warning.
"First" is quite a bit of work, if you want to bring it into a format that Joe
Hurd can understand, assuming he even has the time to look into it.
To suppress the warning, one trick is to ensure that the theorem has no name
hint, e.g.
mythm[THEN asm_rl]
or (if it's not polymorphic) pipe it in with "using mythm apply -". The first
trick could be made cleaner through a new attribute, e.g. "silent" or
"nameless".
I'd rather not add any feature directly to "metis" because it's unlikely to be
discovered by the few users who will run into the issue, and care -- but I
encourage you to experiment with this, and if your idiom spreads so that it has
more than one user we could consider it for inclusion in Isabelle [*].
Cheers,
Jasmin
[*] A rule of thumb I remember from industry was to wait until we had the same
feature request at least three times before implementing anything. That of
course made more sense w.r.t. a large user base (~ 10 000 to 100 000) than for
the Isabelle community.
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
