From 3616445f9a60402701ca00a22e9e6e2fbe95c741 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Fri, 7 Mar 2014 15:18:24 +0100
Subject: add a Functor structure

The intent is to replace some uses of Vec with a structure that also
happens to be a functor. RawFunctors from the standard library provide
no laws though, so we define a Functor structure that adds the laws. As
an additional law congruence is added, because

 * Other standard library structures in Algebra.Structures also require
   congruence.
 * Otherwise the identity law would have to reason about different
   identities.
---
 Everything.agda | 1 +
 1 file changed, 1 insertion(+)

(limited to 'Everything.agda')

diff --git a/Everything.agda b/Everything.agda
index e37c76e..7383dd5 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -2,6 +2,7 @@
 module Everything where
 
 import Generic
+import Structures
 import FinMap
 import CheckInsert
 import GetTypes
-- 
cgit v1.2.3