------------------------------------------------------------------------
-- The Agda standard library
--
-- Data.Vec.Any.Membership instantiated with propositional equality,
-- along with some additional definitions.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Vec.Membership.Propositional {a} {A : Set a} where
open import Data.Vec.Base using (Vec)
open import Data.Vec.Relation.Unary.Any using (Any)
open import Relation.Binary.PropositionalEquality.Core using (subst)
open import Relation.Binary.PropositionalEquality.Properties using (setoid)
import Data.Vec.Membership.Setoid as SetoidMembership
------------------------------------------------------------------------
-- Re-export contents of setoid membership
open SetoidMembership (setoid A) public hiding (lose)
------------------------------------------------------------------------
-- Other operations
lose : ∀ {p} {P : A → Set p} {x n} {xs : Vec A n} → x ∈ xs → P x → Any P xs
lose = SetoidMembership.lose (setoid A) (subst _)
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