In Hitchiker's Guide to Logical Verification (2023 Standard Edition) Ch. 2, p. 16, we have this --
"The general format of recursive definitions is:
def name (params1 : type1) . . . (params-m : type-m) : type
| patterns1 => result1
...
| patterns-n => result-n
The parameters params1 to params-m cannot be subjected to pattern matching, only the remaining arguments declared in 'type'."
However, in "Functional Programming in Lean", Sec. 1.6 "Polymorphism", we find this example:
def length (α : Type) (xs : List α) : Nat :=
match xs with
| List.nil => Nat.zero
| List.cons y ys => Nat.succ (length α ys)
as well as this one:
def List.head? {α : Type} (xs : List α) : Option α :=
match xs with
| [] => none
| y :: _ => some y
In both of the latter 2 cases, the match expression references parameters that appear in the header parameters, i.e. before the colon, as opposed to the overall type spec which appears after the colon.
Another apparent inconsistency -- in the Hitchiker's version, there is no 'match' statement; the alternates appear directly after the header.
What's the correct understanding here?
The first excerpt is incorrect. Recursive definitions are allowed to use match expressions in Lean 4. It looks like this was overlooked when the book was translated from Lean 3.
Both the syntax from the Hitchhiker's Guide and FPIL are allowed. For example, the second code block is equivalent to
def length (α : Type) : List α -> Nat
| List.nil => Nat.zero
| List.cons y ys => Nat.succ (length α ys)