coq - Coq 中的范围 - 导入时没有解析？

Question

考虑示例代码：

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？

标签： coq

Answer 1

该Import命令可以帮助：

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