From dab051e89bbe904587a047d239e79610554d5c91 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Mon, 10 Mar 2014 08:17:41 +0100
Subject: implement a bff on a shaped source type

Add IsShaped and Shaped records describing shapely types as in Jay95.
Implement bff on Shaped and rewrite PartialVecVec to use the vector
shape retaining all proofs on the vector implementation.
---
 Instances.agda | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 Instances.agda

(limited to 'Instances.agda')

diff --git a/Instances.agda b/Instances.agda
new file mode 100644
index 0000000..faff6f8
--- /dev/null
+++ b/Instances.agda
@@ -0,0 +1,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
+    } }
-- 
cgit v1.2.3