[isabelle-dev] »real« considered harmful
makarius at sketis.net
Wed Jun 24 21:01:45 CEST 2015
On Wed, 24 Jun 2015, Larry Paulson wrote:
> This may be the problem. I don’t remember exactly what I was trying to
> do, only that it was very difficult. Of course nobody uses show_types
> any more. Larry
>> On 24 Jun 2015, at 15:13, Dmitriy Traytel <traytel at in.tum.de> wrote:
>> You can hover in the output panel, but you won't see types of constants
Input and output of terms have always been slightly asymmetric, despite
attempts to make them agree as much as feasible over the decades.
The type annotations for certain term items in the PIDE document markup is
only half finished. It was considered impossible over many years, and
getting it to the still current state was so difficult, that I did not
revisit it again. It needs to be done one day, nonetheless.
Note that show_types is actually related to PIDE type markup: roughly
speaking, in places where show_types could work, the markup can be
provided as well.
More information about the isabelle-dev