*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] A course based on Isabelle/HOL and some feedback...*From*: Thomas Genet <thomas.genet at irisa.fr>*Date*: Fri, 27 Apr 2012 09:26:58 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1204261713490.24124@macbroy21.informatik.tu-muenchen.de>*References*: <4F99585C.5090003@irisa.fr> <alpine.LNX.2.00.1204261713490.24124@macbroy21.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7; rv:12.0) Gecko/20120420 Thunderbird/12.0

Le 26/04/12 17:21, Makarius a écrit :

This is one of these scoping errors that then lead to a conflict with the type constraints imposed by already defined entities, and are thus discovered indirectly. The type checking phase could be a bit more ambitious to maintain precise position information and report that (which is technically not so easy and might require one or two more release cycles to materialize).

But the actual scoping is already represented quite nicely in current Isabelle2011-1 right now, if you use Isabelle/jEdit and rely in its "Haribo effect". This means the sources are painted in funny colors according to the role of identifiers. The Prover IDE also has the magic CONTROL (or COMMAND) key, which asks the system to explain the formal status of some piece of source. So the above "id" would have come out black (constant) instead of the expected blue (free variable), and its tooltip would have said "constant Fun.id", with a hyperlink to jump to its definition in main HOL. So students would have to spend less energy divinating the meaning of the text themselves.

Best regards, Thomas -- Thomas Genet ISTIC/IRISA Campus de Beaulieu, 35042 Rennes cedex, France Tél: +33 (0) 2 99 84 73 44 E-mail: genet at irisa.fr http://www.irisa.fr/celtique/genet

**References**:**[isabelle] A course based on Isabelle/HOL and some feedback...***From:*Thomas Genet

**Re: [isabelle] A course based on Isabelle/HOL and some feedback...***From:*Makarius

- Previous by Date: Re: [isabelle] Product or function?
- Next by Date: Re: [isabelle] A course based on Isabelle/HOL and some feedback...
- Previous by Thread: Re: [isabelle] A course based on Isabelle/HOL and some feedback...
- Next by Thread: Re: [isabelle] A course based on Isabelle/HOL and some feedback...
- Cl-isabelle-users April 2012 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