From f80becc368cbda11806bd7ecbb20d65b6d57d02e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Sun, 30 May 2021 20:10:16 +0100 Subject: [PATCH] Spell out anonymous function notation --- thesis.tex | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/thesis.tex b/thesis.tex index 6bbc56a..3cf31be 100644 --- a/thesis.tex +++ b/thesis.tex @@ -2325,7 +2325,10 @@ synonymous. For a function $f : A \to B$ (or partial function $f : A \pto B$) we write $f(a) = b$ to mean $(a, b) \in f$, and say that $f$ applied to -$a$ returns $b$. The notation $f(a)$ means the application of $f$ to +$a$ returns $b$. We write $f(P) \defas M$ for the definition of a +function with pattern $P$ and expression $M$, and sometimes we will +use the anonymous notation $P \mapsto M$ to mean $f(P) \defas M$ for +some fresh $f$. The notation $f(a)$ means the application of $f$ to $a$, and we say that $f(a)$ is defined whenever $f(a) = b$ for some $b$. %