使用coqtop检查表达式的类型

Question

我很好奇Coq实体的类型等同于逻辑中的连接词.为了特殊性,让我们说->和/\.如果->是一个神奇的非[第一类实体],那么让我们只使用它/\作为实体.我很好奇它的域名是Prop还是Set.

是否可以使用coqtop获取表达式的类型？

我想用ghci做类似于以下的事情.

> ghci
:GHCi, version 8.6.3:  :? for help
Prelude> :t (**)
(**) :: Floating a => a -> a -> a

Answer 1

/\并且->都是符号,而不是Coq中的实际常量.要找到他们的签名,您必须首先确定它们的符号.运行命令Locate "/\".应输出一些内容

Notation
"A /\ B" := and A B : type_scope
(default interpretation)

这/\是常数的表示法and.然后,您可以使用该命令Check查找其类型.Check and.给

and
     : Prop -> Prop -> Prop

所以and需要两个Props并给出一个Prop.

同样,A -> B是一种表示法forall _: A, B.不同于and,forall不是常量,而是Coq语言中的关键字,因此您无法使用Check forall.获取签名.在这种情况下,您可以查看产品的参考手册并查看

表达式forall ident : type, term表示该术语ident的类型变量的乘积.至于抽象, 后面跟一个活页夹列表,几个变量的产品相当于一个变量产品的迭代.请注意,这是一种类型.typetermforallterm

因此,这意味着这两个A和B应该是类型,这意味着它们可以是任何宇宙的元素Prop,Set或Type.