Coq输入功率问题

Question

• 看来我无法正确安装Coq导入系统。
• 我在pow_succ_r中找到了Coq.Arith.PeanoNat。
• 所以我导入了它并希望它可以使用

Require Import Coq.Arith.PeanoNat.
Print pow_succ_r.

我收到以下错误：

pow_succ_r not a defined object.

Answer 1

注意文档顶部附近的Module Nat行。这意味着后续的声明在Nat模块内部。因此，您可以将符号访问为Nat.pow_succ_r。

通常，如果您要寻找符号，请使用Locate命令：

Locate pow_succ_r.
(*
Constant
  Coq.Arith.PeanoNat.Nat.pow_succ_r
  (shorter name to refer to it in current context is Nat.pow_succ_r)
*)