From 3b50410ec0a8b83344d0f61df554a1024bdaf298 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Dvo=C5=99=C3=A1k?= Date: Sat, 4 Mar 2023 11:19:25 +0100 Subject: [PATCH] doc: typo --- doc/lean3changes.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/lean3changes.md b/doc/lean3changes.md index 10c41c68ad..e97e9066af 100644 --- a/doc/lean3changes.md +++ b/doc/lean3changes.md @@ -85,7 +85,7 @@ def id5 : {α : Type} → α → α := ## Sugar for simple functions -In Lean 3, we can create simple functions from infix operators by using parentheses. For example, `(+1)` is sugar for `fun x, x + 1`. In Lean 4, we generalize this notation using `·` As a placeholder. Here are a few examples: +In Lean 3, we can create simple functions from infix operators by using parentheses. For example, `(+1)` is sugar for `fun x, x + 1`. In Lean 4, we generalize this notation using `·` as a placeholder. Here are a few examples: ```lean # namespace ex3