diff options
Diffstat (limited to 'Generic.agda')
| -rw-r--r-- | Generic.agda | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/Generic.agda b/Generic.agda index 061042f..3106c5f 100644 --- a/Generic.agda +++ b/Generic.agda @@ -24,9 +24,6 @@ open Category.Monad.RawMonad {Level.zero} Data.Maybe.Categorical.monad using (_> ≡-to-Π : {A B : Set} → (A → B) → P.setoid A ⟶ P.setoid B ≡-to-Π f = record { _⟨$⟩_ = f; cong = P.cong f } -just-injective : {A : Set} → {x y : A} → Maybe.just x ≡ Maybe.just y → x ≡ y -just-injective P.refl = P.refl - 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) |