diff options
| author | Iain Lane <laney@debian.org> | 2011-11-29 16:51:32 +0000 |
|---|---|---|
| committer | Iain Lane <laney@debian.org> | 2011-11-29 16:51:32 +0000 |
| commit | becce68e992af760dbdc6f17e77bc4dfeecccef7 (patch) | |
| tree | fe929e2d8863fe17c1c2909283e1442b6f4a3286 /src/Data/Fin/Dec.agda | |
| parent | 9251e0b00e309e805a4576ae558b3d1e321d8f2c (diff) | |
Imported Upstream version 0.6~darcs20111129t1640
Diffstat (limited to 'src/Data/Fin/Dec.agda')
| -rw-r--r-- | src/Data/Fin/Dec.agda | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/src/Data/Fin/Dec.agda b/src/Data/Fin/Dec.agda index d54ca0c..0bee913 100644 --- a/src/Data/Fin/Dec.agda +++ b/src/Data/Fin/Dec.agda @@ -1,9 +1,9 @@ ------------------------------------------------------------------------ +-- The Agda standard library +-- -- Decision procedures for finite sets and subsets of finite sets ------------------------------------------------------------------------ -{-# OPTIONS --universe-polymorphism #-} - module Data.Fin.Dec where open import Function @@ -11,7 +11,7 @@ import Data.Bool as Bool open import Data.Nat hiding (_<_) open import Data.Vec hiding (_∈_) open import Data.Vec.Equality as VecEq - using () renaming (module HeterogeneousEquality to HetVecEq) + using () renaming (module PropositionalEquality to PropVecEq) open import Data.Fin open import Data.Fin.Subset open import Data.Fin.Subset.Props @@ -19,7 +19,6 @@ open import Data.Product as Prod open import Data.Empty open import Function import Function.Equivalence as Eq -open import Level hiding (Lift) open import Relation.Binary import Relation.Binary.HeterogeneousEquality as H open import Relation.Nullary @@ -170,6 +169,5 @@ infix 4 _⊆?_ _⊆?_ : ∀ {n} → Decidable (_⊆_ {n = n}) p₁ ⊆? p₂ = Dec.map (Eq.sym NaturalPoset.orders-equivalent) $ - Dec.map′ H.≅-to-≡ H.≡-to-≅ $ - Dec.map′ HetVecEq.to-≅ HetVecEq.from-≅ $ + Dec.map′ PropVecEq.to-≡ PropVecEq.from-≡ $ VecEq.DecidableEquality._≟_ Bool.decSetoid p₁ (p₁ ∩ p₂) |