>> 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:
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
> 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
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
