gpt4 book ai didi

import - 对 Coq 进口感到困惑

转载 作者:行者123 更新时间:2023-12-04 14:25:48 25 4
gpt4 key购买 nike

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

  • Require姓名。
  • Require Import姓名。
  • Import姓名

  • ?

    最佳答案

  • Require : 加载一个外部库(通常来自标准库或 user-contribs/ 文件夹);
  • Import : 导入模块中的名称。例如,如果您有一个函数 f在一个模块中 M , 通过执行 Import M. ,您只需输入 f而不是 M.f ;
  • Require Import : 两者都有RequireImport .
  • 关于import - 对 Coq 进口感到困惑,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/33854672/

    25 4 0
    Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
    广告合作:1813099741@qq.com 6ren.com