考虑示例代码：
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？
该Import命令可以帮助：
From Coq Require Import BinNat.
Import N.
About ones.
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句