------------------------------------------------------------------------
-- The Agda standard library
--
-- Universal lifting of predicates over Vectors
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Vec.Functional.Relation.Unary.All where
open import Data.Fin.Properties using (all?)
open import Data.Product.Base using (_,_)
open import Data.Vec.Functional as VF hiding (map)
open import Level using (Level)
open import Relation.Unary using (Pred; _⊆_; Decidable; Universal; Satisfiable)
private
variable
a p q ℓ : Level
A : Set a
------------------------------------------------------------------------
-- Definition
All : Pred A ℓ → ∀ {n} → Vector A n → Set ℓ
All P xs = ∀ i → P (xs i)
------------------------------------------------------------------------
-- Operations
module _ {P : Pred A p} {Q : Pred A q} where
map : P ⊆ Q → ∀ {n} → All P {n = n} ⊆ All Q
map p⊆q ps i = p⊆q (ps i)
------------------------------------------------------------------------
-- Properties of predicates preserved by All
module _ {P : Pred A p} where
all : Decidable P → ∀ {n} → Decidable (All P {n = n})
all p? xs = all? λ i → p? (xs i)
universal : Universal P → ∀ {n} → Universal (All P {n = n})
universal uni xs i = uni (xs i)
satisfiable : Satisfiable P → ∀ {n} → Satisfiable (All P {n = n})
satisfiable (x , px) = (λ _ → x) , (λ _ → px)
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