From 04e312472d4737815cf6c37258b547673faa0b91 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Sun, 25 Nov 2018 08:54:51 +0100
Subject: fix missing import of "length"

Broken in parent commit.
---
 Generic.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Generic.agda')

diff --git a/Generic.agda b/Generic.agda
index fab3a25..9046ebb 100644
--- a/Generic.agda
+++ b/Generic.agda
@@ -2,7 +2,7 @@ module Generic where
 
 import Category.Functor
 import Category.Monad
-open import Data.List using (List) renaming ([] to []L ; _∷_ to _∷L_)
+open import Data.List using (List ; length) renaming ([] to []L ; _∷_ to _∷L_)
 open import Data.Maybe using (Maybe ; just ; nothing) renaming (setoid to MaybeEq)
 open import Data.Nat using (ℕ ; zero ; suc)
 open import Data.Product using (_×_ ; _,_)
-- 
cgit v1.2.3