diff options
Diffstat (limited to 'Data/Vector/Monoid.agda')
| -rw-r--r-- | Data/Vector/Monoid.agda | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/Data/Vector/Monoid.agda b/Data/Vector/Monoid.agda index da09de9..7205800 100644 --- a/Data/Vector/Monoid.agda +++ b/Data/Vector/Monoid.agda @@ -12,15 +12,17 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Data.Nat using (ℕ) open import Data.Product using (_,_) -open import Data.Vec using (Vec; foldr′; zipWith; replicate) +open import Data.Vec using (Vec; foldr′; zipWith; replicate; _++_) open import Data.Vector.Core M.setoid as S using (Vector; _≊_; module ≊; pull; Vectorₛ) +open import Data.Vector.Vec using (replicate-++) +open import Relation.Binary.PropositionalEquality using (_≡_) open M open Vec private variable - n A B C : ℕ + n m A B C : ℕ opaque @@ -54,6 +56,9 @@ opaque ⟨ε⟩ : Vector n ⟨ε⟩ {n} = replicate n ε + ⟨ε⟩-++ : ⟨ε⟩ {n} ++ ⟨ε⟩ {m} ≡ ⟨ε⟩ + ⟨ε⟩-++ {n} {m} = replicate-++ n m ε + opaque unfolding _⊕_ ⟨ε⟩ @@ -95,9 +100,9 @@ open import Categories.Object.Monoid Setoids-×.monoidal as Obj using (Monoid⇒ open import Data.Fin using (Fin) open import Data.Monoid using (module FromMonoid) open import Data.Monoid {c} {c ⊔ ℓ} using (fromMonoid) -open import Data.Vec using (tabulate; lookup) +open import Data.Vec using (tabulate; lookup; _++_) open import Data.Vec.Properties using (tabulate-cong; lookup-zipWith; lookup-replicate) -open import Data.Vector.Vec using (zipWith-tabulate; replicate-tabulate) +open import Data.Vector.Vec using (zipWith-tabulate; replicate-tabulate; replicate-++) open import Function using (Func; _⟨$⟩_; _∘_; id) open import Relation.Binary.PropositionalEquality as ≡ using (module ≡-Reasoning; _≡_; _≗_) |