diff options
Diffstat (limited to 'Generic.agda')
| -rw-r--r-- | Generic.agda | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/Generic.agda b/Generic.agda index 11b9594..2ef374c 100644 --- a/Generic.agda +++ b/Generic.agda @@ -7,7 +7,7 @@ open import Data.Maybe using (Maybe ; just ; nothing) open import Data.Nat using (ℕ ; zero ; suc) open import Data.Product using (_×_ ; _,_) open import Data.Vec using (Vec ; toList ; fromList ; map) renaming ([] to []V ; _∷_ to _∷V_) -open import Function using (_∘_) +open import Function using (_∘_ ; id) import Level open import Relation.Binary.Core using (_≡_ ; refl) open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ; trans) @@ -23,7 +23,7 @@ just-injective : {A : Set} → {x y : A} → Maybe.just x ≡ Maybe.just y → x just-injective refl = refl length-replicate : {A : Set} {a : A} → (n : ℕ) → length (replicate n a) ≡ n -length-replicate zero = refl +length-replicate zero = refl length-replicate (suc n) = cong suc (length-replicate n) map-just-injective : {A : Set} {n : ℕ} {xs ys : Vec A n} → @@ -46,6 +46,15 @@ mapMV-purity : {A B : Set} {n : ℕ} → (f : A → B) → (v : Vec A n) → map mapMV-purity f []V = refl mapMV-purity f (x ∷V xs) rewrite mapMV-purity f xs = refl +sequenceV : {A : Set} {n : ℕ} → Vec (Maybe A) n → Maybe (Vec A n) +sequenceV = mapMV id + +sequence-map : {A B : Set} {n : ℕ} → (f : A → Maybe B) → sequenceV {n = n} ∘ map f ≗ mapMV f +sequence-map f []V = refl +sequence-map f (x ∷V xs) with f x +sequence-map f (x ∷V xs) | just y = cong (_<$>_ (_∷V_ y)) (sequence-map f xs) +sequence-map f (x ∷V xs) | nothing = refl + subst-cong : {A : Set} → (T : A → Set) → {g : A → A} → {a b : A} → (f : {c : A} → T c → T (g c)) → (p : a ≡ b) → f ∘ subst T p ≗ subst T (cong g p) ∘ f subst-cong T f refl _ = refl |