From 2d33726c69f299634fc1776328f297d08e0a4c31 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Martin=20Dvo=C5=99=C3=A1k?= <martin.dvorak@matfyz.cz>
Date: Fri, 5 May 2023 21:19:19 +0200
Subject: [PATCH] doc: `f(x)` is no longer allowed (#2135)

---
 doc/lean3changes.md | 2 ++
 1 file changed, 2 insertions(+)

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,