From 211368cf29790fbd26455b66550216fce2d4f93c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Mon, 11 Mar 2019 07:12:48 +0100 Subject: [PATCH] Lists: fixes the symbol for the cons operator --- src/plfa/Lists.lagda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/Lists.lagda b/src/plfa/Lists.lagda index bc949a6d..68f0b6c8 100644 --- a/src/plfa/Lists.lagda +++ b/src/plfa/Lists.lagda @@ -54,7 +54,7 @@ For example, _ : List ℕ _ = 0 ∷ 1 ∷ 2 ∷ [] \end{code} -denotes the list of the first three natural numbers. Since `_::_` +denotes the list of the first three natural numbers. Since `_∷_` associates to the right, the term parses as `0 ∷ (1 ∷ (2 ∷ []))`. Here `0` is the first element of the list, called the _head_, and `1 ∷ (2 ∷ [])` is a list of the remaining elements, called the