We discussed the issue here and the consensus was to adopt your naming
convention uniformly: t_eqI and t_eq_iff
I will wait a few days before I do anything about it to see if there are
negative reactions.
If not, then the new names will replace the old ones (except for the
axiom "ext").
Tobias
For compatibility, I will follow Michael and reintroduce the old names
as synonyms. I am unsure about other types. For HOLCF functions the
ext_iff scheme makes sense, too, but I would leave that to you.
Concerning products: I agree we should get rid of "Pair_fst_snd_iff" and
"complex_Re_Im_canc
On 08/09/10 05:04, Brian Huffman wrote:
OK, this makes sense. It is nice to have the pair of lemmas "foo_ext"
and "foo_ext_iff" for each function-like type "foo".
So do you propose that we rename all of the expand_*_eq lemmas that I
listed before? (It would also be good to make sure there is a
p
OK, this makes sense. It is nice to have the pair of lemmas "foo_ext"
and "foo_ext_iff" for each function-like type "foo".
So do you propose that we rename all of the expand_*_eq lemmas that I
listed before? (It would also be good to make sure there is a
properly-named *_ext lemma corresponding to
I wanted to emphasize the mathematical concept, not the operational
view. And indeed, it is shorter. For functional objects the ext_iff
convention fits perfectly. For example, for polynomials we already have
poly_ext in one direction. I have to admit, though, that for pairs it
would be a bit un
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 lemma
___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
