Hi Gerwin, > Do I read find_eta.txt right that the eta expansion is applied to all patterns? If yes, then that is a problem, because now partially applied constants won’t be found any more (i.e. the occurrence of `Suc` in `map Suc ?xs` would be missed if you make it always search for `Suc _`).
It is not eta-expansion. It is an expansion of abstractions, e.g.
%f. inj_on f UNIV ~> inj_on _ UNIV
but not
Suc ~/~> Suc _
> Also, always eta-contracting the pattern is not necessarily a good idea.
> The user might have specifically used the non-contracted form to exclude
> matches she is not interested in
> (e.g. might specifically not want `map Suc ?xs`).
It is proper eta-contraction and thus only affecting abstractions. E.g.
%n. Suc n ~> Suc
but not
Suc _ ~/~> Suc
I played a little bit in my head with the semantic consequences and
judged them quite consistent and convenient. But maybe I have
overlooked significant counterexamples.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
