From af1ea86b6e817a85d4d160833fc5d4bb89e2df7b Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 23 Jan 2014 13:19:02 +0100 Subject: generalize BFF and theorem-2 to arbitrary Setoids Since the generalization of lemma-checkInsert-restrict there is nothing to show for theorem-1. So everything works with Setoids now yielding the same results as the paper proofs. --- BFF.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'BFF.agda') diff --git a/BFF.agda b/BFF.agda index 984528a..88d9244 100644 --- a/BFF.agda +++ b/BFF.agda @@ -2,7 +2,7 @@ module BFF where open import Data.Nat using (ℕ) open import Data.Fin using (Fin) -import Level +open import Level using () renaming (zero to ℓ₀) import Category.Monad import Category.Functor open import Data.Maybe using (Maybe ; just ; nothing ; maybe′) @@ -11,16 +11,16 @@ open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) 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 Relation.Binary using (DecSetoid ; module DecSetoid) open import FinMap import CheckInsert import FreeTheorems -module VecBFF (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where +module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where open FreeTheorems.VecVec public using (get-type) - open CheckInsert (decSetoid deq) + open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq) + open CheckInsert A assoc : {n m : ℕ} → Vec (Fin n) m → Vec Carrier m → Maybe (FinMapMaybe n Carrier) assoc []V []V = just empty -- cgit v1.2.3