diff options
Diffstat (limited to 'src/Wasm/Util/List/Map/Any.agda')
| -rw-r--r-- | src/Wasm/Util/List/Map/Any.agda | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/Wasm/Util/List/Map/Any.agda b/src/Wasm/Util/List/Map/Any.agda new file mode 100644 index 0000000..196ecc5 --- /dev/null +++ b/src/Wasm/Util/List/Map/Any.agda @@ -0,0 +1,12 @@ +{-# OPTIONS --safe --without-K #-} + +module Wasm.Util.List.Map.Any where + +open import Data.List using (_∷_) +open import Level using (_⊔_) +open import Relation.Unary using (Pred) +open import Wasm.Util.List.Map + +data Any {a b p} {A : Set a} {B : A → Set b} (P : ∀ {x} → Pred (B x) p) : ∀ {xs} → Pred (Map B xs) (a ⊔ b ⊔ p) where + here : ∀ {x xs y ys} (py : P y) → Any P {x ∷ xs} (y ∷ ys) + there : ∀ {x xs y ys} (pys : Any P ys) → Any P {x ∷ xs} (y ∷ ys) |