[isabelle-dev] Redundant equations in function declarations

[Tobias Nipkow]

Isabelle does not allow you to keep on proving a lemma after you have already
proved all subgoals, although it could just ignore further proof steps, thus
saving you the effort to comment them out...

Tobias

Am 03/06/2012 21:29, schrieb Alexander Krauss:
>> Thank you for investigating. I have been waiting for Alex to present his view.
> 
> Sorry for being late. I've been offline for some days and am a bit behind now :-)
> 
>> Naturally, the current treatment resembles ML's.
> 
> Yes. I don't think there were any further considerations.
> 
> [...]
>> There is no reason to allow a specification to contain material that may
>> contradict another part of the specification.
> 
> Well, the meaning of an equation in the "fun" command is: If the equation
> overlaps with a previous one, consider just the non-overlapping part. And your
> proposed change would be an exception to this rule.
> 
> It does not happen very often, but I have occasionally written thing like this
> myself in intermediate experimentation stages. Eventually, I clean things up of
> course, but having a hard error would force me to comment out more stuff
> temporarily...
> 
> But I understand your concerns.
> 
> Technically, this situation represents a recoverable error (the definition and
> the rest of the theory can be processed), but always indicates a problem in the
> sources that should be fixed. It seems that we do not currently have a
> corresponding severity level. Therefore choosing between "ignored spam warning"
> and "break your leg error" is a bit difficult.
> 
> Questions:
> 
> - Do we need a level for such messages/annotations? In IDE terms, a little
> yellow triangle with an exclamation mark comes to my mind. I wouldn't want to
> see this for most iother warnings, but here it might make sense.
> 
> - @Larry: Do you think your students would have noticed it if the redundant
> equations had been underlined in yellow?
> 
> - @Makarius: Is it already possible for a package to emit a message/report that
> carries position information, say to underline one of the clauses in a
> specification processed by read_specification? This could also improve the error
> reporting in other cases.
> 
> Alex
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev