Re: [isabelle] Unfixed variables in "define" command

On 22/02/2021 13:23, Makarius wrote:
> Further note that our ultra-flexible term syntax makes it impossible to say
> e.g. that "a" wants to bind its argument (in contrast to ML: "fun a x = ...").

Maybe part of the confusion is from mistaking Isabelle/HOL as a functional
programming language, where definitions have a special syntactic status. In
contrast Isabelle definitions are logical specifications based on equations.
(Definitions like 'inductive' are again more general in this respect.)

Here is a fun-fact that may help to see the difference more clearly. The
successor function defined in ML, Haskell, Scala:

  fun a a = a + 1;

  a :: Int -> Int
  a a = a + 1

  def a(a: Int): Int = a + 1

The lambda-term language of the Isabelle logical framework works quite
differently, it cannot (and should) not imitate that.


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