Coq Import problems with power

user_3357352 0
Viewed 48
  • It seems I can't get the Coq Import system right.
  • I found pow_succ_r in Coq.Arith.PeanoNat.
  • So I imported it and hoped it is usable
Require Import Coq.Arith.PeanoNat.
Print pow_succ_r.

I get the following error:

pow_succ_r not a defined object.
coq
1 Answers

Notice the line Module Nat near the top of the documentation. It means that the subsequent declarations are inside the Nat module. So, you can access the symbol as Nat.pow_succ_r.

In general, if you are looking for a symbol, use the Locate command:

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)
*)
user_134991210
Related