Introduction to the λ-Calculus

&gt; (according to one rumour, because Dana Scott was fond of curry)<p>I always assumed it was related to Haskell Curry, the logician.

&gt; Extensionality fails in most dependent type theories<p>Is this a reason to use Isabelle?<p>I remember Bob Harper being interested in dependent typing. What is his take on extensionality?

What is the benefitsof the lambda notation over a more intuitive arrow notation like x-&gt;x+1?