*To*: Thomas Genet <thomas.genet at irisa.fr>*Subject*: Re: [isabelle] A course based on Isabelle/HOL and some feedback...*From*: Makarius <makarius at sketis.net>*Date*: Thu, 26 Apr 2012 17:21:52 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4F99585C.5090003@irisa.fr>*References*: <4F99585C.5090003@irisa.fr>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Thu, 26 Apr 2012, Thomas Genet wrote:

-- It is a bad idea to use a variable name like id in a function equation, e.g.: fun f:: "nat => nat" where "f(id)=id" 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.

Makarius

**Follow-Ups**:**Re: [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:*Thomas Genet

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

- Previous by Date: [isabelle] A course based on Isabelle/HOL and some feedback...
- Next by Date: Re: [isabelle] A course based on Isabelle/HOL and some feedback...
- Previous by Thread: [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