代码之家 › 专栏 › 技术社区 › Siddharth Bhat

Coq中的作用域-导入时没有解析?

coq

Siddharth Bhat · 技术社区 · 6 年前

考虑一下示例代码:

Require Import BinNat.
Open Scope N.

Check (N.ones).
(* Error: The reference ones
   was not found in the current environment. *)
Check (ones).

如何导入 BinNat 这样我就不必下决心了 ones 到 N.ones ?

1 回复 | 直到 6 年前

Anton Trunov 6 年前

这个 Import 命令可以帮助:

From Coq Require Import BinNat.
Import N.
About ones.

推荐文章

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 年前