------------------------------------------------------------------------
-- The Agda standard library
--
-- AVL trees where at least one element satisfies a given property
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Bundles using (StrictTotalOrder)
module Data.Tree.AVL.Map.Relation.Unary.Any
{a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
where
open import Data.Product.Base as Product using (_×_; ∃; _,_)
open import Function.Base using (_∘_; _∘′_; id)
open import Level using (Level; _⊔_)
open import Relation.Unary using (Pred; Decidable; Satisfiable; _⊆_; _∪_)
open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
open import Data.Tree.AVL.Map strictTotalOrder using (Map)
open import Data.Tree.AVL.Indexed strictTotalOrder using (toPair)
import Data.Tree.AVL.Relation.Unary.Any strictTotalOrder as Map
private
variable
v p q : Level
V : Set v
P : Pred V p
Q : Pred V q
m : Map V
------------------------------------------------------------------------
-- Definition
-- Given a predicate P, Any P t describes a path in t to an element that
-- satisfies P. There may be others.
-- See `Relation.Unary` for an explanation of predicates.
Any : {V : Set v} → Pred (Key × V) p → Pred (Map V) (a ⊔ ℓ₂ ⊔ v ⊔ p)
Any P = Map.Any (P ∘′ toPair)
------------------------------------------------------------------------
-- Operations on Any
map : P ⊆ Q → Any P ⊆ Any Q
map f = Map.map f
lookup : Any {V = V} P m → Key × V
lookup = toPair ∘′ Map.lookup
lookupKey : Any P m → Key
lookupKey = Map.lookupKey
-- If any element satisfies P, then P is satisfied.
satisfied : Any P m → ∃ P
satisfied = Product.map toPair id ∘′ Map.satisfied
------------------------------------------------------------------------
-- Properties of predicates preserved by Any
any? : Decidable P → Decidable (Any P)
any? P? = Map.any? (P? ∘ toPair)
satisfiable : Satisfiable P → Satisfiable (Any P)
satisfiable ((k , v) , p) = Map.satisfiable k (v , p)
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