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

doc: f(x) is no longer allowed (#2135)

Browse source
This commit is contained in:
Martin Dvořák 2023-05-05 21:19:19 +02:00 • committed by GitHub
parent ebcab266c6
commit 2d33726c69
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/lean3changes.md
View file

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