diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-01-17 09:24:47 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-01-17 09:24:47 +0100 |
| commit | 808b8da4b14b087c0dcace71fff3854a17cebe42 (patch) | |
| tree | 213872ff0a7165dee7a9510f75d78d7b76ccc015 /Precond.agda | |
| parent | 5bf7ce31ca6928b13d6631591371e98933cb0b2d (diff) | |
| download | bidiragda-808b8da4b14b087c0dcace71fff3854a17cebe42.tar.gz | |
generalize checkInsert to arbitrary Setoids
This is another step towards permitting arbitrary Setoids in bff.
Diffstat (limited to 'Precond.agda')
| -rw-r--r-- | Precond.agda | 4 |
1 files changed, 2 insertions, 2 deletions
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 |