← Back to branch summary

~ubuntu-branches/ubuntu/vivid/agda-stdlib/vivid

« back to all changes in this revision

Viewing changes to src/Data/Fin/Dec.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2011-11-29 17:00:35 UTC
  • mfrom: (1.1.3)
  • Revision ID: package-import@ubuntu.com-20111129170035-00v3pq4mmhoo5ulf
Tags: 0.6~darcs20111129t1640-1
* [ef445ab] Imported Upstream version 0.6~darcs20111129t1640
  + Darcs snapshot required for Agda 2.3.0 compatibility
* [f801f83] Update BDs and deps to require Agda 2.3.0
* [c52be90] Use 3.0 (quilt) for bz2 orig

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Fin/Dec.agda
1
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
2
4
-- Decision procedures for finite sets and subsets of finite sets
3
5
------------------------------------------------------------------------
4
6
 
5
 
{-# OPTIONS --universe-polymorphism #-}
6
 
 
7
7
module Data.Fin.Dec where
8
8
 
9
9
open import Function
11
11
open import Data.Nat hiding (_<_)
12
12
open import Data.Vec hiding (_∈_)
13
13
open import Data.Vec.Equality as VecEq
14
 
  using () renaming (module HeterogeneousEquality to HetVecEq)
 
14
  using () renaming (module PropositionalEquality to PropVecEq)
15
15
open import Data.Fin
16
16
open import Data.Fin.Subset
17
17
open import Data.Fin.Subset.Props
19
19
open import Data.Empty
20
20
open import Function
21
21
import Function.Equivalence as Eq
22
 
open import Level hiding (Lift)
23
22
open import Relation.Binary
24
23
import Relation.Binary.HeterogeneousEquality as H
25
24
open import Relation.Nullary
170
169
_⊆?_ : ∀ {n} → Decidable (_⊆_ {n = n})
171
170
p₁ ⊆? p₂ =
172
171
  Dec.map (Eq.sym NaturalPoset.orders-equivalent) $
173
 
  Dec.map′ H.≅-to-≡ H.≡-to-≅ $
174
 
  Dec.map′ HetVecEq.to-≅ HetVecEq.from-≅ $
 
172
  Dec.map′ PropVecEq.to-≡ PropVecEq.from-≡ $
175
173
  VecEq.DecidableEquality._≟_ Bool.decSetoid p₁ (p₁ ∩ p₂)