Coq中的方括号语法[|-Set]是什么？

Question

我有时会在Coq中看到这种语法来表示某些类型/集合，例如在打印有关存在变量的信息时：

?T : [ |- Set]
?T0 : [ x : ?T |- Set ]

我不知道如何搜索这种语法。

这是什么意思？

第一个与

? T : Set

？

Answer 1

假设我们有一个具有特定类型的术语。

Variable B : nat -> nat.
Check B.
(*
B
     : nat -> nat
 *)

如果我们使用创建另一个术语B它可能会或可能不会打字检查，即B true是不能分型。

Fail Check B true.
(*
 Error message:
 The term "true" has type "bool" while it is expected to have type "nat".
 *)

Coq允许使用通配符，然后尝试找出类型本身。

Check B _.
(*
B ?n
     : nat
where
?n : [ |- nat]
 *)

这里的Coq说的类型B _是nat，但仅在参数（命名?n）为类型的假设下nat。或以其他方式说，“假设一个可以推断，下型?n是nat从空语境”。

有时在“旋转门”符号的左侧会发现更多的东西|-。

Variable x:nat.
Check _ x.
(*
?y x
     : ?T@{x:=x}
where
?y : [ |- forall x : nat, ?T] 
?T : [x : nat |- Type] 
*)

上面的下划线被称为?y和类型(?y x)是一个依赖型?T依赖x。?T仅键式（到Type在上下文其中）x是一个nat。如果x不是nat，则?T不是可键入的。