From 808b8da4b14b087c0dcace71fff3854a17cebe42 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Fri, 17 Jan 2014 09:24:47 +0100
Subject: generalize checkInsert to arbitrary Setoids

This is another step towards permitting arbitrary Setoids in bff.
---
 BFF.agda | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'BFF.agda')

diff --git a/BFF.agda b/BFF.agda
index 0cdb231..984528a 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -12,6 +12,7 @@ open import Data.List using (List ; [] ; _∷_ ; map ; length)
 open import Data.Vec using (Vec ; toList ; fromList ; tabulate ; allFin) renaming (lookup to lookupV ; map to mapV ; [] to []V ; _∷_ to _∷V_)
 open import Function using (id ; _∘_ ; flip)
 open import Relation.Binary.Core using (Decidable ; _≡_)
+open import Relation.Binary.PropositionalEquality using (decSetoid)
 
 open import FinMap
 import CheckInsert
@@ -19,7 +20,7 @@ import FreeTheorems
 
 module VecBFF (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where
   open FreeTheorems.VecVec public using (get-type)
-  open CheckInsert Carrier deq
+  open CheckInsert (decSetoid deq)
 
   assoc : {n m : ℕ} → Vec (Fin n) m → Vec Carrier m → Maybe (FinMapMaybe n Carrier)
   assoc []V       []V       = just empty
-- 
cgit v1.2.3