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

Connectives: Use unicode × instead of x

Browse source
This commit is contained in:
Fangyi Zhou 2019-05-06 16:03:15 +01:00 committed by Wen Kokke
parent 2e999b167e
commit 2f3b9a6aff
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/Connectives.lagda
View file

@ -136,7 +136,7 @@ infixr 2 _×_
\end{code}
Thus, `m ≤ n × n ≤ p` parses as `(m ≤ n) × (n ≤ p)`.
Given two types `A` and `B`, we refer to `A x B` as the
Given two types `A` and `B`, we refer to `A × B` as the
_product_ of `A` and `B`. In set theory, it is also sometimes
called the _Cartesian product_, and in computing it corresponds
to a _record_ type. Among other reasons for