From 1fd075440f3f9a671412a7d8d968990094bf783b Mon Sep 17 00:00:00 2001 From: wadler Date: Fri, 10 Jan 2020 11:02:28 -0300 Subject: [PATCH] fixed error in Lists --- src/plfa/part1/Lists.lagda.md | 23 ----------------------- 1 file changed, 23 deletions(-) diff --git a/src/plfa/part1/Lists.lagda.md b/src/plfa/part1/Lists.lagda.md index 8bfe4223..18e816ed 100644 --- a/src/plfa/part1/Lists.lagda.md +++ b/src/plfa/part1/Lists.lagda.md @@ -354,29 +354,6 @@ reverse of the second appended to the reverse of the first: reverse (xs ++ ys) ≡ reverse ys ++ reverse xs -``` -reverse-++-distrib : ∀ xs ys → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs -reverse-++-distrib [] ys = - begin - reverse ([] ++ ys) - ≡⟨⟩ - reverse ys - ≡⟨ sym (++-identityʳ (reverse ys)) ⟩ - reverse ys ++ reverse [] - ∎ -reverse-++-distrib (x ∷ xs) ys = - begin - reverse ((x ∷ xs) ++ ys) - ≡⟨⟩ - reverse (xs ++ ys) ++ [ x ] - ≡⟨ cong (_++ [ x ]) (reverse-++-distrib xs ys) ⟩ - (reverse ys ++ reverse xs) ++ [ x ] - ≡⟨ ++-assoc (reverse ys) (reverse xs) [ x ] ⟩ - reverse ys ++ (reverse xs ++ [ x ]) - ∎ -``` - - #### Exercise `reverse-involutive` (recommended) A function is an _involution_ if when applied twice it acts