Coq输入功率问题

Question

• 看来我搞错了Coq导入系统。
• 我在Coq.Arith.PeanoNat找到了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)
*)