[isabelle] Unfixed variables in "define" command



Prompted by a question from a student of mine, I am wondering why free
argument variables on the left-hand side of a function definition with
"define" have to be fixed manually with "for" for it to work:

define a :: "nat ⇒ nat" where "a x = 2 * x"

When writing it like this, the "x" is not fixed and therefore the
"definition" does not work. When you add a "for x", it seems to work.

Is there a reason for this behaviour? Would it be possible to fix such
variables automatically, mirroring the behaviour of e.g. the
"definition" command?

Manuel

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.