diff options
author | Helmut Grohne <helmut@subdivi.de> | 2018-11-25 08:54:51 +0100 |
---|---|---|
committer | Helmut Grohne <helmut@subdivi.de> | 2018-11-25 08:54:51 +0100 |
commit | 04e312472d4737815cf6c37258b547673faa0b91 (patch) | |
tree | 101eb3d51b6cbd8a9a5309364e4b978798ea90be /Generic.agda | |
parent | c98062b949a6fc792b042e04453b0bed27941caa (diff) | |
download | bidiragda-04e312472d4737815cf6c37258b547673faa0b91.tar.gz |
fix missing import of "length"
Broken in parent commit.
Diffstat (limited to 'Generic.agda')
-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 (_×_ ; _,_) |