From 5ae3b56ccc4874c5455fde613cb9a0e300628bfa Mon Sep 17 00:00:00 2001 From: Mo Mirza Date: Wed, 11 Sep 2019 00:32:52 +0100 Subject: [PATCH] Fix typo: argument to arguments --- src/plfa/part1/Naturals.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part1/Naturals.lagda.md b/src/plfa/part1/Naturals.lagda.md index c2a31e52..d7af4553 100644 --- a/src/plfa/part1/Naturals.lagda.md +++ b/src/plfa/part1/Naturals.lagda.md @@ -309,7 +309,7 @@ zero + n = n ``` Let's unpack this definition. Addition is an infix operator. It is -written with underbars where the argument go, hence its name is +written with underbars where the arguments go, hence its name is `_+_`. The first line is a signature specifying the type of the operator. The type `ℕ → ℕ → ℕ`, indicates that addition accepts two naturals and returns a natural. Infix notation is just a shorthand for application;