diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-01-28 09:30:45 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-01-28 09:30:45 +0100 |
| commit | f767ec96fec169907da5cb5029852732cf333e7b (patch) | |
| tree | 4844591ccb644defdf054949de5e87078fd0c3a6 /CheckInsert.agda | |
| parent | 8cc43c2c7e5ab40394a1e6a23470edb3d2d6b909 (diff) | |
| download | bidiragda-f767ec96fec169907da5cb5029852732cf333e7b.tar.gz | |
use the indexed version of the Vec Setoid
Diffstat (limited to 'CheckInsert.agda')
| -rw-r--r-- | CheckInsert.agda | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/CheckInsert.agda b/CheckInsert.agda index 47af215..c8007ec 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -18,7 +18,6 @@ import Relation.Binary.EqReasoning as EqR open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans) open import FinMap -open import Generic using (vecIsSetoid) private open module A = DecSetoid A using (Carrier ; _≈_) renaming (_≟_ to deq) |