fix missing import of "length"
authorHelmut Grohne <helmut@subdivi.de>
Sun, 25 Nov 2018 07:54:51 +0000 (08:54 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Sun, 25 Nov 2018 07:54:51 +0000 (08:54 +0100)
Broken in parent commit.

Generic.agda

index fab3a25..9046ebb 100644 (file)
@@ -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 (__ ; _,_)