I am marking some student work submitted for the Cambridge Isabelle course, and have seen some examples where students have gone terribly wrong because they overlooked the warning “Ignoring redundant equation" in a function definition. This sort of mistake could happen to anybody, and it means that proofs are being undertaken on the basis of a mistaken definition. Somebody reading the theory could also overlook this mistake, which goes against the idea that structured proofs should be readable without being executed.
I propose that this particular warning should become a fatal error. Warnings are appropriate for situations that are difficult to avoid, such as overlapping patterns. They might be appropriate for situations that are common and generally harmless, such as missing patterns. But entirely superfluous equations should be seen as a fatal error. This should be a very easy change to implement. Larry _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
