Am 29/05/2012 14:20, schrieb Lawrence Paulson: > 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.
Sounds reasonable. Tobias > 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
