Re: [isabelle-dev] popup in ce6320b9ef9b
>> Here is a minimal example, but I am at loss to explain what is going on >> here. > > The usual reason for a term being annotated twice is that it is (type) > checked twice. Good to know. Maybe a double-check somewhere in the interpretation machinery. 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
Re: [isabelle-dev] popup in ce6320b9ef9b
Here is a minimal example, but I am at loss to explain what is going on here. Florian Am 18.11.2015 um 10:03 schrieb Tobias Nipkow: > In more than one example of locale interpretations with "where f = g", > where g is a constant, if I hover over the g, the popup shows the type > of g twice. > > Tobias > > > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de Where.thy Description: application/extension-thy signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] popup in ce6320b9ef9b
> Here is a minimal example, but I am at loss to explain what is going on > here. The usual reason for a term being annotated twice is that it is (type) checked twice. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] popup in ce6320b9ef9b
In more than one example of locale interpretations with "where f = g", where g is a constant, if I hover over the g, the popup shows the type of g twice. Tobias smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
