From 4a1e4ab42e2076fb00a265a02db37d75d78917f3 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Mon, 13 Nov 2023 11:37:43 +0100 Subject: [PATCH] Update README.md --- README.md | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index ae2a1544..fa05f8ec 100644 --- a/README.md +++ b/README.md @@ -76,11 +76,10 @@ We highlight two syntactical differences. Conveniently, we can write `f : X → Y` to mean "`f` has type `X → Y`", in other words "`f` is a function from `X` to `Y`". -* Secondly, type theorists do not use the mapsto symbol (`↦`), - but instead use lambda-notation. +* Secondly, type theorists use lambda-notation. This means that we can define the square function on the integers via - `λ x, x^2`, which translates to `x ↦ x^2` in set-theoretic notation. - For more information about `λ`, see the Wikipedia page on + `fun x ↦ x^2`, which translates to `x ↦ x^2` in set-theoretic notation. + For more information about `λ` (called `fun` in Lean 4), see the Wikipedia page on [lambda calculus](https://en.wikipedia.org/wiki/Lambda_calculus). For a more extensive discussion of type theory,