------------------------------------------------------------------------
-- The Agda standard library
--
-- Membership relation for AVL Maps identifying values up to
-- propositional equality.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Bundles using (StrictTotalOrder)
module Data.Tree.AVL.Map.Membership.Propositional
{a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
where
open import Data.Product.Base using (_×_)
open import Data.Product.Relation.Binary.Pointwise.NonDependent
using ()
renaming (Pointwise to _×ᴿ_)
open import Level using (Level)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
open import Relation.Nullary.Negation.Core using (¬_)
open StrictTotalOrder strictTotalOrder using (_≈_) renaming (Carrier to Key)
open import Data.Tree.AVL.Map strictTotalOrder using (Map)
open import Data.Tree.AVL.Map.Relation.Unary.Any strictTotalOrder using (Any)
private
variable
v : Level
V : Set v
m : Map V
kx : Key × V
infix 4 _≈ₖᵥ_
_≈ₖᵥ_ : Rel (Key × V) _
_≈ₖᵥ_ = _≈_ ×ᴿ _≡_
------------------------------------------------------------------------
-- Membership: ∈ₖᵥ
infix 4 _∈ₖᵥ_ _∉ₖᵥ_
_∈ₖᵥ_ : Key × V → Map V → Set _
kx ∈ₖᵥ m = Any (_≈ₖᵥ_ kx) m
_∉ₖᵥ_ : Key × V → Map V → Set _
kx ∉ₖᵥ m = ¬ kx ∈ₖᵥ m
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