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

TSPL: a few spelling error fixes in PUC Assignment 2

Browse source
This commit is contained in:
Marko Dimjašević 2019-07-05 22:45:40 +02:00 committed by Wen Kokke
parent 715e81af59
commit ae503a2534
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
tspl/PUC-Assignment2.lagda
View file

@ -60,7 +60,7 @@ open import plfa.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
The proof of monotonicity from The proof of monotonicity from
Chapter [Relations][plfa.Relations] Chapter [Relations][plfa.Relations]
can be written in a more readable form by using an anologue of our can be written in a more readable form by using an analogue of our
notation for `≡-reasoning`. Define `≤-reasoning` analogously, and use notation for `≡-reasoning`. Define `≤-reasoning` analogously, and use
it to write out an alternative proof that addition is monotonic with it to write out an alternative proof that addition is monotonic with
regard to inequality. Rewrite both `+-monoˡ-≤` and `+-mono-≤`. regard to inequality. Rewrite both `+-monoˡ-≤` and `+-mono-≤`.
@ -131,7 +131,7 @@ Show sum is commutative up to isomorphism.
#### Exercise `⊎-assoc` #### Exercise `⊎-assoc`
Show sum is associative up to ismorphism. Show sum is associative up to isomorphism.
#### Exercise `⊥-identityˡ` (recommended) #### Exercise `⊥-identityˡ` (recommended)
@ -415,7 +415,7 @@ data Tree (A B : Set) : Set where
leaf : A → Tree A B leaf : A → Tree A B
node : Tree A B → B → Tree A B → Tree A B node : Tree A B → B → Tree A B → Tree A B
\end{code} \end{code}
Define a suitabve map operator over trees. Define a suitable map operator over trees.
\begin{code} \begin{code}
postulate postulate
map-Tree : ∀ {A B C D : Set} map-Tree : ∀ {A B C D : Set}
@ -460,7 +460,7 @@ postulate
#### Exercise `map-is-fold-Tree` #### Exercise `map-is-fold-Tree`
Demonstrate an anologue of `map-is-foldr` for the type of trees. Demonstrate an analogue of `map-is-foldr` for the type of trees.
#### Exercise `sum-downFrom` (stretch) #### Exercise `sum-downFrom` (stretch)