{-# 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)