title: Problem with types in a definition in lean
body: <p>If I make the definition</p>
  
  <pre><code>definition f (x : nat) := λ m, x + m
  </code></pre>
  
  <p>then <code>#check f</code> returns <code>f:nat -&gt; nat -&gt; nat</code>, as expected.</p>
  
  <p>If instead I try to define</p>
  
  <pre><code>definition f (x : nat) : nat -&gt; nat -&gt; nat := λ m, x + m
  </code></pre>
  
  <p>then Lean complains, and that x has type <code>nat</code> but is expected to have type <code>nat -&gt; nat</code>.</p>
  
  <p>Why is this?</p>