diff --git a/doc/lean3changes.md b/doc/lean3changes.md index e97e9066af..15da5b89b8 100644 --- a/doc/lean3changes.md +++ b/doc/lean3changes.md @@ -196,6 +196,8 @@ example (f : Nat → Nat) (a b c : Nat) : f (a + b + c) = f (a + (b + c)) := congrArg f (Nat.add_assoc ..) ``` +In Lean 4, writing `f(x)` in place of `f x` is no longer allowed. + ## Dependent function types Given `α : Type` and `β : α → Type`, `(x : α) → β x` denotes the type of functions `f` with the property that,