diff options
Diffstat (limited to 'src/Data/List/Membership/Propositional.agda')
| -rw-r--r-- | src/Data/List/Membership/Propositional.agda | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/src/Data/List/Membership/Propositional.agda b/src/Data/List/Membership/Propositional.agda new file mode 100644 index 0000000..0de5e55 --- /dev/null +++ b/src/Data/List/Membership/Propositional.agda @@ -0,0 +1,24 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Data.List.Any.Membership instantiated with propositional equality, +-- along with some additional definitions. +------------------------------------------------------------------------ + +module Data.List.Membership.Propositional {a} {A : Set a} where + +open import Data.List.Any using (Any) +open import Relation.Binary.PropositionalEquality using (setoid; subst) + +import Data.List.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 xs} → x ∈ xs → P x → Any P xs +lose = SetoidMembership.lose (setoid A) (subst _) |