标准库中是否定义了列表中的元素数据类型？

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