関数の本体から引数の型を推論する仕組みについて

超マニアックな仕様なので書く必要はなさそう

namespace Hidden

-- 型をフルに注釈したバージョン
def id {X : Type} (x : X) : X := x

-- 引数の括弧は実は省略することができる
def id' X x := (x : X)

-- 返り値の型を省略することができる
def id₂ {X : Type} (x : X) := x

-- 関数の本体から、引数 x の型を推論することができる
def id₃ {X : Type} x := (x : X)

-- 返り値の型を注釈すると、「関数の本体を読んで引数の型を推論する」ということが行われなくなり、
-- 引数の型がわからなくてエラーになる。
/--
error: failed to infer binder type
when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed
-/
#guard_msgs in def id₄ {X : Type} x : X := (x : X)

end Hidden

Start by reviewing the Lean snippets in the issue and the repository's existing example structure; no target file or test is named. Confirm whether this niche type-inference behavior belongs in the book, then document it in the appropriate example if accepted and verify it with the project's normal checks.