代码之家 › 专栏 › 技术社区 › user9335697

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

coq

user9335697 · 技术社区 · 8 年前

我在写一首单曲 .v 我发现用如下参数和定义来定义事物很方便:

Parameter n : nat.
Definition n_plus_1 := n + 1.

而不是 Definition n_plus_1 (n : nat) = n + 1.

我的用例比这更复杂,但想法是一样的。虽然用参数定义事物帮助我编写了一些我感兴趣的证明,但有时我只想用实际值测试定义,以确保它们实际计算出我想要的结果。举个例子,我刚才写的例子,我做不到 Compute n_plus_1 3 。在某种意义上,我想实例化参数 n 。最好的方法是什么?

1 回复 | 直到 8 年前

ejgallego 8 年前

最快的方法是使用 Section 机制[模块也可以工作]:

Section With_N.
Variable n : nat.
Definition n_plus_1 := n + 1.
End With_N.

Compute (n_plus_1 3).

推荐文章

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

8 年前

Jason Hu · 参见Ltac中的Hintbase

8 年前

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

8 年前

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

8 年前

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

8 年前

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

8 年前

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

8 年前

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

8 年前

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

8 年前

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

8 年前