agda - 标准库中是否定义了列表中的元素数据类型?
问题描述
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
这是 for Vec
,但我找不到类似的 for List
。
解决方案
它以更通用的形式在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
推荐阅读
- elixir - 在挂载期间使用 LiveView 将值从客户端传递到 Phoenix 服务器
- mongodb - 如何在 Windows 上更改 mongodb 数据目录
- c# - C# 获取 ClassName:异常 TargetSite.DeclaringType.Name 与 MethodBase.GetCurrentMethod().DeclaryingType
- alpine - xxd 在 alpine linux 上没有做任何事情
- ruby-on-rails - SAML IDP 实施以支持单个 IDP 中的多个 SP
- python - 无论如何要截取整个控制台窗口的屏幕截图吗?
- python - 在R中制作时间序列数据框
- mysql - 如何从 IntelliJ IDEA 2018 中的 mysql 转储中恢复 mysql 数据库?
- javascript - React Form 不更新状态 onChange
- django - 为什么我收到 NoReverseMatch 错误,我该如何解决?