max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: typo

Browse source
This commit is contained in:
Martin Dvořák 2023-03-04 11:19:25 +01:00 • committed by GitHub
parent 0da281fab4
commit 3b50410ec0
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/lean3changes.md
View file

@ -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