list - 如何在 Coq 中构建异构依赖对列表

Question

我希望能够有一个异构的依赖对序列在哪里，(T, f)如果T一个函数比如SetfT -> bool

Definition classif :
  seq (forall T : Set, T -> bool) :=
  [:: (fun b : bool => b); (fun n : nat => false)].

注意：我对列表使用 SSReflect 语法。显然上面写的类型不是正确的。

可能吗 ？

标签： listtypescoq

Answer 1

您正在寻找依赖对并且正在编写依赖函数。指向类型的类型是

{ A : Set & A }

然后，您可以构建例如一对natand 1：

Check (existT (fun A : Set => A) nat 1) : { A : Set & A }.

有一些符号会更好，但你有它。