Instances.agda


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

module Instances where

open import Data.Nat using (ℕ)
open import Data.Vec using (Vec)
open import Function using (id)
open import Relation.Binary.PropositionalEquality using (refl)

open import Structures using (Shaped)

VecShaped : Shaped ℕ Vec
VecShaped = record
  { arity = id
  ; content = id
  ; fill = λ _ → id
  ; isShaped = record
    { content-fill = λ _ → refl
    ; fill-content = λ _ _ → refl
    } }