Re: [isabelle] A course based on Isabelle/HOL and some feedback...
On Thu, 26 Apr 2012, Thomas Genet wrote:
-- It is a bad idea to use a variable name like id in a function
fun f:: "nat => nat"
OK, the error message says:
*** Type error in application: incompatible operand type
*** Operator: f :: nat => nat
*** Operand: id :: ??'a => ??'a
and a (careful) student may understand that 'id' is already defined as a
function etc... however this is far more difficult to find when the
function has 10 complex equations.
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and