diff options
Diffstat (limited to 'CheckInsert.agda')
| -rw-r--r-- | CheckInsert.agda | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/CheckInsert.agda b/CheckInsert.agda index dbba6e6..68f5fdb 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -13,7 +13,7 @@ open import Data.Vec.Properties using (lookup∘update′) open import Relation.Nullary using (Dec ; yes ; no ; ¬_) open import Relation.Nullary.Negation using (contradiction) open import Relation.Binary using (Setoid ; module DecSetoid) -import Relation.Binary.EqReasoning as EqR +import Relation.Binary.Reasoning.Setoid as EqR open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≢_ ; inspect ; [_] ; module ≡-Reasoning) open import FinMap |