← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Data/List/All.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/All.agda
13
13
open import Level
14
14
open import Relation.Nullary
15
15
import Relation.Nullary.Decidable as Dec
16
 
open import Relation.Unary using () renaming (_⊆_ to _⋐_)
 
16
open import Relation.Unary using (Decidable) renaming (_⊆_ to _⋐_)
17
17
open import Relation.Binary.PropositionalEquality
18
18
 
19
19
-- All P xs means that all elements in xs satisfy P.
50
50
map g (px ∷ pxs) = g px ∷ map g pxs
51
51
 
52
52
all : ∀ {a p} {A : Set a} {P : A → Set p} →
53
 
      (∀ x → Dec (P x)) → (xs : List A) → Dec (All P xs)
 
53
      Decidable P → Decidable (All P)
54
54
all p []       = yes []
55
55
all p (x ∷ xs) with p x
56
56
all p (x ∷ xs) | yes px = Dec.map′ (_∷_ px) tail (all p xs)