Introduce type-safe instances and threadsHEADmaster

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)