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

Minor clarifications on exercises in Naturals and Induction.

Browse source
This commit is contained in:
Wen Kokke 2020-01-21 17:03:56 +00:00
parent 0003b0465f
commit 29dc9321d8
2 changed files with 9 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/plfa/part1/Induction.lagda.md
View file

@ -75,13 +75,11 @@ that a newly introduced operator is associative but not commutative.
Give another example of a pair of operators that have an identity Give another example of a pair of operators that have an identity
and are associative, commutative, and distribute over one another. and are associative, commutative, and distribute over one another.
(You do not have to prove these properties.)
Give an example of an operator that has an identity and is Give an example of an operator that has an identity and is
associative but is not commutative. associative but is not commutative.
(You do not have to prove these properties.)
```
-- Your code goes here
```
## Associativity ## Associativity
@ -944,9 +942,9 @@ for all naturals `m`, `n`, and `p`.
Show the following three laws Show the following three laws
m ^ (n + p) ≡ (m ^ n) * (m ^ p) m ^ (n + p) ≡ (m ^ n) * (m ^ p) (^-distribˡ-+-*)
(m * n) ^ p ≡ (m ^ p) * (n ^ p) (m * n) ^ p ≡ (m ^ p) * (n ^ p) (^-distribʳ-*)
m ^ (n * p) ≡ (m ^ n) ^ p (m ^ n) ^ p ≡ m ^ (n * p) (^-*-assoc)
for all `m`, `n`, and `p`. for all `m`, `n`, and `p`.

7
src/plfa/part1/Naturals.lagda.md
View file

@ -428,7 +428,7 @@ other word for evidence, which we will use interchangeably, is _proof_.
#### Exercise `+-example` (practice) {#plus-example} #### Exercise `+-example` (practice) {#plus-example}
Compute `3 + 4`, writing out your reasoning as a chain of equations. Compute `3 + 4`, writing out your reasoning as a chain of equations, using the equations for `+`.
``` ```
-- Your code goes here -- Your code goes here
@ -489,7 +489,8 @@ it can easily be inferred from the corresponding term.
#### Exercise `*-example` (practice) {#times-example} #### Exercise `*-example` (practice) {#times-example}
Compute `3 * 4`, writing out your reasoning as a chain of equations. Compute `3 * 4`, writing out your reasoning as a chain of equations, using the equations for `*`.
(You do not need to step through the evaluation of `+`.)
``` ```
-- Your code goes here -- Your code goes here
@ -566,7 +567,7 @@ _ =
∎ ∎
``` ```
#### Exercise `∸-examples` (recommended) {#monus-examples} #### Exercise `∸-example₁` and `∸-example₂` (recommended) {#monus-examples}
Compute `5 ∸ 3` and `3 ∸ 5`, writing out your reasoning as a chain of equations. Compute `5 ∸ 3` and `3 ∸ 5`, writing out your reasoning as a chain of equations.