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

Lists: fixes spellings of several words

Browse source
This commit is contained in:
Marko Dimjašević 2019-01-24 21:05:26 +01:00 committed by Wen Kokke
parent e3623f18cb
commit 2a33fefab0
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
extra/extra/Lists-backup.lagda
View file

@ -284,7 +284,7 @@ length-++ (x ∷ xs) ys =
length (x ∷ xs) + length ys
∎
\end{code}
The proof is by induction on the first arugment. The base case instantiates
The proof is by induction on the first argument. The base case instantiates
to `[]`, and follows by straightforward computation.
As before, Agda cannot infer the implicit type parameter to `length`,
and it must be given explicitly.

6
src/plfa/Lists.lagda
View file

@ -283,7 +283,7 @@ length-++ (x ∷ xs) ys =
length (x ∷ xs) + length ys
∎
\end{code}
The proof is by induction on the first arugment. The base case
The proof is by induction on the first argument. The base case
instantiates to `[]`, and follows by straightforward computation. As
before, Agda cannot infer the implicit type parameter to `length`, and
it must be given explicitly. The inductive case instantiates to
@ -655,7 +655,7 @@ postulate
#### 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)
@ -958,7 +958,7 @@ All? P? (x ∷ xs) with P? x | All? P? xs
\end{code}
If the list is empty, then trivially `P` holds for every element of
the list. Otherwise, the structure of the proof is similar to that
showing that the conjuction of two decidable propositions is itself
showing that the conjunction of two decidable propositions is itself
decidable, using `_∷_` rather than `⟨_,_⟩` to combine the evidence for
the head and tail of the list.