From 9a746a0b0e9f1143a8f3922473f91c47a3af665b Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 31 Aug 2021 10:28:46 +0100
Subject: Introduce type-safe instances and threads

---
 src/Wasm/Util/List/Map/Any.agda | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 src/Wasm/Util/List/Map/Any.agda

(limited to 'src/Wasm/Util/List/Map')

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)
-- 
cgit v1.2.3