Suggestion: more thorough summary of function definition alternatives

It was a little bit confusing at first that Lean has different ways of specifying the types of functions. At first I assumed that they were simply alternative, equivalent syntaxes. At first I thought I would write functions like this because I came to Lean from Idris, Agda, and Haskell:

def f1 : (x : Int) → (y: Int) → Int :=
  x - y

This fails because x and y are unbound in the body of the function definition. So one needs to move the argument terms before the type colon:

def f2 (x : Int) (y : Int) : Int :=
  x - y

I figured that out by trial and error, though. Yet f2 has the type Int -> Int -> Int. I finally realized that putting parameters before the colon is like using (defn f [x] ...) rather than (def g (fn [x] ...) in Clojure, or like (define (f x) ...) vs. (define f (lambda [x] ...) in Scheme.

Of course there are lots of examples in FPIL using arguments before the colon, but I didn't know why that choice was made. This point might be somewhere in FPIL and I missed it, but I haven't found it in section 1.3--the obvious place. Maybe that's because 1.3 is part of an introductory overview, but in that case would it be worth having a "More on functions" section somewhere, which summarized different ways of defining functions and their implications? Maybe the material on pattern-matching definitions and implicit arguments from section 1.7 could also be moved there.

(I also thought that maybe it wasn't necessary for FPIL to summarize the semantics of different function definition syntaxes, because that sort of systematic overview is what one often finds in a language manual. However, section 3.2.1 of the manual (in the beta you linked to from Zulip), which seems like it might be where such a thing is found, is partially opaque to me, and it's not clear to me whether what the features discussed above are even implied by what's there. I assume that the purpose of the manual is deeper than providing a reference that can be used by someone who's started to get their feet wet with Lean, which is fine, as long as there are other resources. Hence the suggestion for FPIL.)

Thanks!

Review FPIL sections 1.3 and 1.7, then compare the relevant treatment with section 3.2.1 of the Lean manual. Done means FPIL clearly explains the different function-definition forms, their implications, and where pattern matching and implicit arguments fit.