>> The abstraction expansion would basically mean you can’t search for >> abstractions at all any more. I.e. even something like (%_. _) would be >> expanded into (_ _). That’s not necessarily catastrophic, but probably >> counter-intuitive. >> >> Has anyone apart from me ever searched for an abstraction that was not an >> abbreviation? If yes, why? > > Well, there are parts of the system without implicit eta-conversion, and > some with. I personally would not bother about find patterns working > modulo eta-conversion implicitly.
Silence has fallen on this thread. Let me put the matter into a more
technical shape.
As it is »by now«, search patterns in find_theorems are not matched
modulo eta-conversion.
I see two technical solutions to resolve this:
a) Make the underlying pattern match implementation work modulo
eta-conversion.
b) Expand the search patterns themselves, as proposed above.
Why I have been reluctant to implement a) is that this would complicate
a potentially time-critical code. Hence the more pragmatic solution b).
So, which path is better to follow from now? In case of doubt, we can
choose b) and still later get back to it.
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
