Adapted to standard-library 1.5 (closes #7)

effectfully · Jan 27, 2021 · 380554b · 380554b
1 parent 3d20000
commit 380554b
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/generic.agda-lib b/generic.agda-lib
@@ -1,3 +1,3 @@
-name: generic-0.1
+name: generic-0.1.0.2
 depend: standard-library
 include: src
diff --git a/readme.md b/readme.md
@@ -2,7 +2,7 @@
 
 It's a library for doing generic programming in Agda.
 
-The library is tested with Agda-2.6.1 and likely does not work with other versions of Agda.
+The library is tested with Agda-2.6.1 and Agda-2.6.1.2 and likely does not work with other versions of Agda.
 
 # A quick taste
 

diff --git a/src/Generic/Lib/Data/Sum.agda b/src/Generic/Lib/Data/Sum.agda
@@ -1,3 +1,3 @@
 module Generic.Lib.Data.Sum where
 
-open import Data.Sum hiding (swap) renaming (map to smap) hiding (map₁; map₂; assocʳ; assocˡ) public
+open import Data.Sum hiding (swap) renaming (map to smap) hiding (map₁; map₂; assocʳ; assocˡ; reduce) public