implement a bff on a shaped source type
[~helmut/bidiragda.git] / Instances.agda
1 module Instances where
2
3 open import Data.Nat using (ℕ)
4 open import Data.Vec using (Vec)
5 open import Function using (id)
6 open import Relation.Binary.PropositionalEquality using (refl)
7
8 open import Structures using (Shaped)
9
10 VecShaped : Shaped ℕ Vec
11 VecShaped = record
12   { arity = id
13   ; content = id
14   ; fill = λ _ → id
15   ; isShaped = record
16     { content-fill = λ _ → refl
17     ; fill-content = λ _ _ → refl
18     } }