通過勒柯克困惑進口

Question

是否有人可以告訴我

• Require名稱之間的差異。
• Require Import名稱。
• Import名稱

？

Answer 1

• Require：（從標準庫或user-contribs/文件夾通常）加載一個外部庫;
• Import：在模塊中導入名稱。例如，如果您在模塊M中通過執行Import M.而具有功能f，則只需鍵入f而不是M.f;
• Require Import：既有Require又有Import。