------------------------------------------------------------------------
-- The Agda standard library
--
-- Existential lifting of predicates over Vectors
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Vec.Functional.Relation.Unary.Any where
open import Data.Fin.Base using (zero; suc)
open import Data.Fin.Properties using (any?)
open import Data.Nat.Base using (ℕ)
open import Data.Product.Base as Σ using (Σ; ∃; _×_; _,_; proj₁; proj₂)
open import Data.Vec.Functional as VF hiding (map)
open import Function.Base using (id)
open import Level using (Level)
open import Relation.Unary using (Pred; _⊆_; Decidable)
private
variable
a b p q ℓ : Level
A : Set a
B : Set b
------------------------------------------------------------------------
-- Definition
Any : Pred A ℓ → ∀ {n} → Vector A n → Set ℓ
Any P xs = ∃ λ i → P (xs i)
------------------------------------------------------------------------
-- Operations
module _ {P : Pred A p} where
here : ∀ {x n} {v : Vector A n} → P x → Any P (x ∷ v)
here px = zero , px
there : ∀ {x n} {v : Vector A n} → Any P v → Any P (x ∷ v)
there = Σ.map suc id
module _ {P : Pred A p} {Q : Pred A q} where
map : P ⊆ Q → ∀ {n} → Any P {n = n} ⊆ Any Q
map p⊆q = Σ.map id p⊆q
------------------------------------------------------------------------
-- Properties of predicates preserved by Any
module _ {P : Pred A p} where
any : Decidable P → ∀ {n} → Decidable (Any P {n = n})
any p? xs = any? λ i → p? (xs i)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4