diff options
| -rw-r--r-- | Generic.agda | 2 |
1 files changed, 1 insertions, 1 deletions
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 (_×_ ; _,_) |