被Coq进口混淆

Question

有人可以告诉我之间的区别

• Require 名字.
• Require Import 名字.
• Import 名称

？

Answer 1

• Require:加载外部库(通常来自标准库或user-contribs/文件夹);
• Import:导入模块中的名称.例如,如果你有一个功能f模块中M,通过这样做Import M.,你只需要输入f代替M.f;
• Require Import:做Require和两个Import.