Lists.agda

module plfa.Lists where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_)
open import Data.Product using (_×_; proj₁; proj₂; ∃; ∃-syntax)
  renaming (_,_ to ⟨_,_⟩)
open import plfa.Isomorphism using (_≃_)

data List (A : Set) : Set where
  []  : List A
  _∷_ : A → List A → List A

infixr 5 _∷_

data Any {A : Set} (P : A → Set) : List A → Set where
  here  : ∀ {x : A} {xs : List A} → P x → Any P (x ∷ xs)
  there : ∀ {x : A} {xs : List A} → Any P xs → Any P (x ∷ xs)

infix 4 _∈_

_∈_ : ∀ {A : Set} (x : A) (xs : List A) → Set
x ∈ xs = Any (x ≡_) xs

Any-∃ : ∀ {A : Set} {P : A → Set} (xs : List A)
      → Any P xs ≃ (∃[ x ∈ xs ] P x)
Any-∃ xs = ?

{-
/home/collares/plfa/Lists.agda:25,21-36
Could not parse the application ∃[ x ∈ xs ] P x
Operators used in the grammar:
∈    (infix operator, level 4)   [_∈_ (/home/collares/plfa/Lists.agda:21,1-4)]
∃[_] (prefix notation, level 20) [∃-syntax (/home/collares/.cabal/agda-stdlib-1.0.1/src/Data/Product.agda:40,1-9)]
when scope checking ∃[ x ∈ xs ] P x
-}