diff options
Diffstat (limited to 'Generic.agda')
| -rw-r--r-- | Generic.agda | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/Generic.agda b/Generic.agda index 9f1172d..fab3a25 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 ; length ; replicate) renaming ([] to []L ; _∷_ to _∷L_) +open import Data.List using (List) 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 (_×_ ; _,_) @@ -27,10 +27,6 @@ open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_) just-injective : {A : Set} → {x y : A} → Maybe.just x ≡ Maybe.just y → x ≡ y just-injective refl = refl -length-replicate : {A : Set} {a : A} → (n : ℕ) → length (replicate n a) ≡ n -length-replicate zero = refl -length-replicate (suc n) = cong suc (length-replicate n) - sequenceV : {A : Set} {n : ℕ} → Vec (Maybe A) n → Maybe (Vec A n) sequenceV []V = just []V sequenceV (x ∷V xs) = x >>= (λ y → (_∷V_ y) <$> sequenceV xs) |