michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Lists: fixes the symbol for the cons operator

Browse source
This commit is contained in:
Marko Dimjašević 2019-03-11 07:12:48 +01:00 committed by Wen Kokke
parent daaf2f9b82
commit 211368cf29
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/plfa/Lists.lagda
View file

@ -54,7 +54,7 @@ For example,
_ : List ℕ _ : List ℕ
_ = 0 ∷ 1 ∷ 2 ∷ [] _ = 0 ∷ 1 ∷ 2 ∷ []
\end{code} \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 ∷ []))`. associates to the right, the term parses as `0 ∷ (1 ∷ (2 ∷ []))`.
Here `0` is the first element of the list, called the _head_, Here `0` is the first element of the list, called the _head_,
and `1 ∷ (2 ∷ [])` is a list of the remaining elements, called the and `1 ∷ (2 ∷ [])` is a list of the remaining elements, called the