Re: [isabelle] [Fwd: Something strange with simplifier and (op \<circ>)]



At the moment it isn't easy to tell whether terms are eta-contracted or not, and if you reset the flag, terms can become unreadable.

However, this problem mainly seems to affect (f\<circ>g).

Larry

On 7 Nov 2007, at 15:04, Peter Lammich wrote:

Yes, it is exactly that. And the expansion to "%x. (f\<circ>g) x" was
done by the induct - method (no idea why, and why only at some places).
All in all this makes coping with lemmas like list.map_compose rather
counter-intuitive. Are there some general guidelines how one
should/could circumvent stuff like this or do I simply have to live with it.

Many thanks for pointing me to that (I did not even know that terms are
displayed eta-contracted by default)






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.