Added foldr-++ foldl-++ and map-cong2 to Data.List.Properties and tid…

…ied up the file
agda · Jun 26, 2017 · 5727880 · 5727880
1 parent 5eb5d9a
commit 5727880
Show file tree

Hide file tree

Showing 2 changed files with 151 additions and 163 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -88,7 +88,8 @@ Important changes since 0.13:
 
 * Added `+-left-identity` and `*-left-zero` to `Data.Nat.Properties.Simple`
 
-* Added `reverse-length` to `Data.List.Properties`
+* Added `length-reverse`, `foldr-++`, `foldl-++` and `map-cong₂`
+  to `Data.List.Properties`
 
 * Changed `Data.Vec.All.All₂` to a native version which allows better
   pattern matching. The new version (and the associated proofs in