[isabelle-dev] NEWS: expand_fun_eq -> ext_iff, expand_set_eq -> set_ext_iff
brianh at cs.pdx.edu
Tue Sep 7 17:22:41 CEST 2010
The log message, "Naming in line now with multisets" seems to suggest
that consistency was the main motivation for this change. However, the
change had rather the opposite effect, since the expand_*_eq pattern
is much more common in the libraries. (Full disclosure: some, but not
all, of these lemmas were named by me.)
Meanwhile, multiset_ext_iff was the only example of the *_ext_iff form
I could find.
If naming consistency was the primary goal here, then I think it would
have been much better to just rename multiset_ext_iff to
expand_multiset_eq. (Alternatively, you could try to consistently
change everything to the "ext_iff" style, but "complex_ext_iff" or
"prod_ext_iff" would be a bit weird.)
Personally, I also like the expand_*_eq naming style because it is
descriptive: When you see "simp add: expand_fun_eq" in a proof, there
is no ambiguity about which way the rule is oriented.
On the other hand, the "ext_iff" names are shorter.
On Tue, Sep 7, 2010 at 3:06 AM, Tobias Nipkow <nipkow at in.tum.de> wrote:
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev