crypto-agda/crypto-agda forked from np/crypto-agda

Data/Tree/Binary/Perfect/Any.agda

• Loading branch information...
1 parent ea9aaed commit 54d8dc027f6ebe86986e35cd77afa0637fa7c890 np committed May 3, 2012
Showing with 23 additions and 0 deletions.
1. +23 −0 Data/Tree/Binary/Perfect/Any.agda
23 Data/Tree/Binary/Perfect/Any.agda
 @@ -0,0 +1,23 @@ +module Data.Tree.Binary.Perfect.Any where + +open import Level +open import Relation.Binary.PropositionalEquality +open import prefect-bintree + +data Any {a p} {A : Set a} (P : A → Set p) : ∀ {n} → Tree A n → Set (a ⊔ p) where + leaf : ∀ {x} (Px : P x) → Any P (leaf x) + left : ∀ {n} {t₀ t₁ : Tree A n} → Any P t₀ → Any P (fork t₀ t₁) + right : ∀ {n} {t₀ t₁ : Tree A n} → Any P t₁ → Any P (fork t₀ t₁) + +pattern here = Any.leaf + +data All {a p} {A : Set a} (P : A → Set p) : ∀ {n} → Tree A n → Set (a ⊔ p) where + leaf : ∀ {x} (Px : P x) → All P (leaf x) + fork : ∀ {n} {t₀ t₁ : Tree A n} → All P t₀ → All P t₁ → All P (fork t₀ t₁) + +_∈_ : ∀ {a} {A : Set a} (x : A) {n} → Tree A n → Set a +x ∈ t = Any (_≡_ x) t + +lookup : ∀ x t → Dec (x ∈ t) + +P ⇒ Q → All P t → All Q (map f t)

0 comments on commit 54d8dc0

Please sign in to comment.