[isabelle-dev] Redundant equations in function declarations

[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