通过勒柯克困惑进口

Question

是否有人可以告诉我

• Require名称之间的差异。
• Require Import名称。
• Import名称

？

Answer 1

• Require：（从标准库或user-contribs/文件夹通常）加载一个外部库;
• Import：在模块中导入名称。例如，如果您在模块M中通过执行Import M.而具有功能f，则只需键入f而不是M.f;
• Require Import：既有Require又有Import。