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

Capitalises 'cartesian'

Browse source
This commit is contained in:
Marko Dimjašević 2019-01-24 09:12:29 +01:00 committed by Wen Kokke
parent 0460f4c415
commit aa1a49d336
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
extra/extra/Logic.lagda
View file

@ -94,7 +94,7 @@ Thus, `m ≤ n × n ≤ p` parses as `(m ≤ n) × (n ≤ p)` and
Given two types `A` and `B`, we refer to `A x B` as the Given two types `A` and `B`, we refer to `A x B` as the
*product* of `A` and `B`. In set theory, it is also sometimes *product* of `A` and `B`. In set theory, it is also sometimes
called the *cartesian product*, and in computing it corresponds called the *Cartesian product*, and in computing it corresponds
to a *record* type. Among other reasons for to a *record* type. Among other reasons for
calling it the product, note that if type `A` has `m` calling it the product, note that if type `A` has `m`
distinct members, and type `B` has `n` distinct members, distinct members, and type `B` has `n` distinct members,

2
src/plfa/Connectives.lagda
View file

@ -133,7 +133,7 @@ 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 x B` as the
_product_ of `A` and `B`. In set theory, it is also sometimes _product_ of `A` and `B`. In set theory, it is also sometimes
called the _cartesian product_, and in computing it corresponds called the _Cartesian product_, and in computing it corresponds
to a _record_ type. Among other reasons for to a _record_ type. Among other reasons for
calling it the product, note that if type `A` has `m` calling it the product, note that if type `A` has `m`
distinct members, and type `B` has `n` distinct members, distinct members, and type `B` has `n` distinct members,