← Back to branch summary

~ubuntu-branches/ubuntu/utopic/agda-stdlib/utopic-proposed

« back to all changes in this revision

Viewing changes to src/Data/List/Any.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2011-12-30 20:02:46 UTC
  • mfrom: (1.1.4)
  • Revision ID: package-import@ubuntu.com-20111230200246-xl31fi4bnippohay
Tags: 0.6-1
* [a88bdc0] Imported Upstream version 0.6
* [7aea5f2] Update copyright for new copyright holders and for new DEP5

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/List/Any.agda
17
17
open import Level using (Level; _⊔_)
18
18
open import Relation.Nullary
19
19
import Relation.Nullary.Decidable as Dec
20
 
open import Relation.Unary using () renaming (_⊆_ to _⋐_)
21
 
open import Relation.Binary
 
20
open import Relation.Unary using (Decidable) renaming (_⊆_ to _⋐_)
 
21
open import Relation.Binary hiding (Decidable)
22
22
import Relation.Binary.InducedPreorders as Ind
23
23
open import Relation.Binary.List.Pointwise as ListEq using ([]; _∷_)
24
24
open import Relation.Binary.PropositionalEquality as PropEq
48
48
-- Decides Any.
49
49
 
50
50
any : ∀ {a p} {A : Set a} {P : A → Set p} →
51
 
      (∀ x → Dec (P x)) → (xs : List A) → Dec (Any P xs)
 
51
      Decidable P → Decidable (Any P)
52
52
any p []       = no λ()
53
53
any p (x ∷ xs) with p x
54
54
any p (x ∷ xs) | yes px = yes (here px)