blob: c7b4a73d160af97f1bb973a96a616a512cb856e4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
{-# OPTIONS --without-K --safe #-}
open import Algebra using (Monoid; CommutativeMonoid)
open import Level using (Level; _⊔_)
module Data.Vector.CommutativeMonoid {c ℓ : Level} (CM : CommutativeMonoid c ℓ) where
module CM = CommutativeMonoid CM
import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
open import Data.Vector.Core CM.setoid using (Vector; _≊_; module ≊)
open import Data.Vector.Monoid CM.monoid as M using (_⊕_)
open import Data.Nat using (ℕ)
open import Data.Vec using (Vec)
open CM
open Vec
private
variable
n : ℕ
opaque
unfolding _⊕_
⊕-comm : (V W : Vector n) → V ⊕ W ≊ W ⊕ V
⊕-comm [] [] = ≊.refl
⊕-comm (v ∷ V) (w ∷ W) = comm v w PW.∷ ⊕-comm V W
-- A commutative monoid of vectors for each natural number
Vectorₘ : ℕ → CommutativeMonoid c (c ⊔ ℓ)
Vectorₘ n = record
{ Monoid (M.Vectorₘ n)
; isCommutativeMonoid = record
{ Monoid (M.Vectorₘ n)
; comm = ⊕-comm
}
}
|
