diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2013-12-17 08:49:24 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2013-12-17 08:49:24 +0100 |
| commit | 88ac52ceabaf2bf4a3f27293a8e04a3daaf8b907 (patch) | |
| tree | 434e67b2e485bee51268cedef1b417424466f958 /Precond.agda | |
| parent | 066861f9cdde4ded6c5442508bef1a27576c68d7 (diff) | |
| download | bidiragda-88ac52ceabaf2bf4a3f27293a8e04a3daaf8b907.tar.gz | |
refactor to get rid of FinMap without Maybe entirely
The union was the only user of this type and now it uses only partial
mappings. So drop remaining uses of FinMap and make everything work with
FinMapMaybe instead.
Diffstat (limited to 'Precond.agda')
| -rw-r--r-- | Precond.agda | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Precond.agda b/Precond.agda index 16e452b..40ffd79 100644 --- a/Precond.agda +++ b/Precond.agda @@ -20,7 +20,7 @@ open import Function using (flip ; _∘_) open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) -open import FinMap using (FinMap ; FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty) +open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty) import CheckInsert open CheckInsert Carrier deq using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other) import BFF |