From 808b8da4b14b087c0dcace71fff3854a17cebe42 Mon Sep 17 00:00:00 2001 From: Helmut Grohne 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. --- Precond.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Precond.agda') diff --git a/Precond.agda b/Precond.agda index e4699dc..41e3407 100644 --- a/Precond.agda +++ b/Precond.agda @@ -17,12 +17,12 @@ open Data.List.Any.Membership-≡ using (_∉_) open import Data.Maybe using (just) open import Data.Product using (∃ ; _,_) open import Function using (flip ; _∘_) -open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym) +open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) open import FinMap using (FinMap ; FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty) import CheckInsert -open CheckInsert Carrier deq using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other) +open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other) import BFF import Bidir -- cgit v1.2.3