*To*: Peter Lammich <lammich at in.tum.de>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Misleading tooltips on Isabelle-Terms with coercions in isabelle/jedit*From*: Dmitriy Traytel <traytel at in.tum.de>*Date*: Tue, 26 Nov 2013 13:38:05 +0100*In-reply-to*: <1385467561.2325.51.camel@lapbroy33>*References*: <1385467561.2325.51.camel@lapbroy33>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.1.1

Am 26.11.2013 13:06, schrieb Peter Lammich:

Hi, when giving the semantics tutorial this morning, I ran into quite strange tooltips in Isabelle/jedit: Consider, theory Scratch imports Complex_Main begin term "∃a::nat. ∃b::real. a+b=0" when hovering over the a in "a+b" and pressing Ctrl, I get the following tooltip: bound "a" bound variable :: real This tooltip is simply wrong! The variable a still has type nat. So I would have expected either a::nat, or "real a :: real".

theory Scratch imports Main begin declare [[coercion_enabled]] declare [[coercion int]] declare [[coercion_map "λf g h. g o h o f"]] term "∃a::nat. ∃b::int. a+b=0" end

Dmitriy

**References**:

- Previous by Date: Re: [isabelle] Stray processes on Windows
- Next by Date: [isabelle] Coercions rename bound variables
- Previous by Thread: [isabelle] Misleading tooltips on Isabelle-Terms with coercions in isabelle/jedit
- Next by Thread: [isabelle] Coercions rename bound variables
- Cl-isabelle-users November 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list