blob: 196ecc5577be117cfaa4a81f659aaa9eb2d44d72 (
plain)
1
2
3
4
5
6
7
8
9
10
11
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)
|
