Существует ли тип элемента в списке, определенный в стандартной библиотеке?

Question

data _[_]=_ {A : Set a} : ∀ {n} → Vec A n → Fin n → A → Set a where
  here  : ∀ {n}     {x}   {xs : Vec A n} → x ∷ xs [ zero ]= x
  there : ∀ {n} {i} {x y} {xs : Vec A n}
          (xs[i]=x : xs [ i ]= x) → y ∷ xs [ suc i ]= x

Это для Vec, но я не могу найти аналог для List.

Answer 1

Доступно в более общей форме в Data.List.Relation.Unary.Any. Вот как это определяется.

data Any {A : Set a} (P : Pred A p) : Pred (List A) (a ⊔ p) where
  here  : ∀ {x xs} (px  : P x)      → Any P (x ∷ xs)
  there : ∀ {x xs} (pxs : Any P xs) → Any P (x ∷ xs)

Вот пример его использования.

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.List
open import Data.List.Relation.Unary.Any

data NonRepeating {a} {A : Set a} : (l : List A) → Set a where
  done : NonRepeating []
  rest : ∀ {x xs} → ¬ Any (x ≡_) xs → NonRepeating xs → NonRepeating (x ∷ xs)

record UniqueList {a} (A : Set a) : Set a where
  constructor _//_
  field
    l : List A
    wf : NonRepeating l