代码之家 › 专栏 › 技术社区 › Greg Nisbet

使用coqtop检查表达式类型

coq

Greg Nisbet · 技术社区 · 6 年前

我很好奇在逻辑上等价于连接词的coq实体的类型。为了特殊性,我们假设 -> 和 /\ . 如果 -gt; 是一个神奇的非一流实体,那我们就用 / \ 作为实体。我很好奇它的域是prop还是set。

可以用吗 coqtop 要获取表达式的类型吗?

我想用ghci做类似的事情。

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

1 回复 | 直到 6 年前

eponier 6 年前

/\ 和 -> 都是符号,而不是coq中的实际常量。要找到他们的签名,你必须首先确定他们是什么符号。运行命令 Locate "/\". 应该沿着

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

所以 / \ 是常量的符号 and . 然后您可以使用命令 Check 找到它的类型。 Check and. 给予

and
     : Prop -> Prop -> Prop

所以 和 拿两个 Prop 给出了一个 支柱 .

同样地, A -> B 是的符号 forall _: A, B . 不像 和 , forall 不是常量,而是coq语言中的关键字,因此不能使用 Check forall. 得到签名。在这种情况下,你可以查一下 the reference manual for products 看到那个

表达式 forall ident : type, term 表示变量 ident 类型的 type 在这个词上 term . 至于摘要, 福尔 后面是活页夹列表,产品超过变量等价于一个变量积的迭代。注意 学期 是一种类型。

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

推荐文章

Mei Zhang · 定义“依赖类型”模函子

7 年前

Jason Hu · 参见Ltac中的Hintbase

7 年前

lllllllllllll · 通过两个实现对阶乘程序进行Coq验证

7 年前

MikkelBybjerg · 如何延迟lambda评估,以便替换lambda

7 年前

user9335697 · 实例化参数以评估函数定义

7 年前

Jian Wang · Coq中的背景目标、搁置目标和放弃目标是什么?

7 年前

Pablo Inostroza · 有没有可能表达一个定理,说明应用了哪些构造函数?

7 年前

jmite · Coq:在校样脚本编写期间查看校样术语

7 年前

ConfusedFormalizer · a是怎样的。vo文件的结构是否便于coqchk使用?

7 年前

Siddharth Bhat · 查看所有已安装的库以及如何在Coq中导入它们

7 年前