程序员经验分享-hwhale

对 Coq 导入感到困惑

2023-11-22

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

  • Require Name.
  • Require Import Name.
  • Import Name

?


  • Require：加载外部库（通常来自标准库或user-contribs/文件夹）;
  • Import：导入模块中的名称。例如，如果你有一个函数f在一个模块中M， 通过做Import M.，您只需要输入f代替M.f;
  • Require Import: 两者都做Require and Import.
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)

import

module

coq

对 Coq 导入感到困惑 的相关文章

随机推荐

  • IndexedDB 性能和 IndexedDB 与 WebSQL 性能比较

    WebSQL 和 IndexedDB 都是用于在 Web 浏览器中访问 CRUD 底层嵌入式数据库的 DB API 如果我没猜错的话 这就像用于访问 CRUD 任何客户端服务器数据库 如 Oracle 等 的 SQL 在许多情况下 同一浏览

  • 属性错误：next()

    我想使用循环一层深度next with os walk 我的代码的关键行 for root dirs files in os walk dir next 1 Error AttributeError 生成器 对象没有属性 下一个 我尝试使用

  • 如何在 React 中使用钩子预先初始化状态？

    基本上在类组件中 我们使用如下所示的初始值在构造函数中预先初始化状态 constructor props super props this state count 0 但是引入钩子之后 所有类组件都变成了带有状态的功能组件 但我的问题是如何

  • 将节点/属性添加到表达式树

    这是我第一次真正处理表达式树 我有点迷失 我很抱歉 如果 这个问题根本没有任何意义 考虑以下类 public class Foo

  • stargazer omit.labels 中的潜在错误

    5 2版本似乎有一个bugstargazer包 其中omit label根据所包含模型的顺序 功能不会一致地工作 library stargazer library ggplot2 as data frame data midwest fi

  • 我可以强制 SoapClient 将数组作为数组返回吗？

    我正在使用 SoapClient 获取一些数据 我从其中一个电话中得到了这个结果 stdClass Object payTransIncome gt stdClass Object item gt stdClass Object payTr

  • 为 iOS 创建 ionic 资源不再有效

    我正在准备我的离子应用程序在 iOS 应用程序商店中进行更新 但我现在真的陷入困境 因为使用生成资源ionic resources不再起作用了 在终端中运行命令后 它开始上传我放入文件夹中的资源 然后告诉我上传已成功完成 然后完全冻结 An

  • 是否可以并行运行同一子项目中的两个独立的 gradle 任务？

    在我工作的项目 基于 gradle 中 有一个非常大的模块 gradle 子项目 在 CI 构建过程中 该子项目中的两个任务按顺序执行 这会导致大量的执行时间 该项目使用org gradle parallel true 但是当我创建简单的项

  • WriteFile 是原子的吗？

    我正在设计一个将时间序列数据写入文件的系统 数据是 8 字节的块 分为两个 4 字节部分 时间和有效负载 根据 MSDN WriteFile 函数是原子的 http msdn microsoft com en us library aa36

  • 如何从函数返回记录集

    我正在 Excel VBA 中构建数据访问层 但在返回记录集时遇到问题 我的类中的 Execute 函数肯定是从数据库中检索一行 但似乎没有返回任何内容 以下函数包含在名为 DataAccessLayer 的类中 该类包含函数 Connec

  • C++98 中的 move() 是什么？

    include

  • 程序接收信号SIGABRT

    我在 iPhone 应用程序中工作 我使用 UIImage 选择器控件从照片库中选取图像 然后处理它并分别使用 UIImageview 和 UITextview 显示图像和相应的输出 对于某些图像 它工作正常 对于某些图像 程序崩溃了 在使

  • 如何检查列表中的两个数字是否相同

    我很好奇如何检查列表中的两个数字是否相同 例如 myList 1 7 9 3 1 2 8 在这种情况下 1 在 myList 中重复 我将如何编写一个程序来检查列表中的两个数字是否相同 重复 尝试使用循环 以便我能够理解 因为我还没有学习复

  • 在实体上显式加载多个引用/集合

    考虑以下实体模型 public class Parent public virtual FirstChild FirstChild get set public virtual SecondChild SecondChild get set

  • 如何在 PHP 中启用跨域 POST？

    我正在将 POST 数据从一个站点发送到另一个站点 这两个站点都是由我们开发的 问题是 如果从另一个域请求该页面 则 POST 变量不可用 即使我在本地测试 但指定完整的url POST数据也没有了 所以 这会起作用

  • MediaRecorder 启动错误代码

    我想录制没有声音并可能进行硬件加速的原始 h 264 视频 并稍后进行流式传输 所以我决定使用MediaRecorder 和插座hack用于流式传输 我有以下代码 final MediaRecorder recorder new Media

  • 计算 ArrayList 中单词的出现次数[重复]

    这个问题在这里已经有答案了 我有一个ArrayList具有重复条目的单词 我想计算并保存数据结构中每个单词的出现次数 我该怎么做 如果您没有大量的字符串列表 那么实现它的最短方法是使用Collections frequency方法 像这样

  • 为什么我的程序在内存不足时偶尔会出现段错误而不是抛出 std::bad_alloc？

    我有一个程序 它实现了几种启发式搜索算法和几个领域 旨在通过实验评估各种算法 该程序用C 编写 使用GNU工具链构建 并在64位Ubuntu系统上运行 当我进行实验时 我使用 bashulimit命令限制进程可以使用的虚拟内存量 以便我的测

  • 在 MySQL (InnoDB) 中查找最佳匹配行

    我有以下测试字符串engine mail key和一个看起来像这样的表 query engine engine pdf engine mail 我想找到最匹配的行 最佳匹配由字符串 行开头的最匹配字符指定 我已经构建了一个 RegExp 但

  • 对 Coq 导入感到困惑

    有人可以告诉我之间的区别吗 Require Name Require Import Name Import Name Require 加载外部库 通常来自标准库或user contribs 文件夹 Import 导入模块中的名称 例如 如果

热门标签