程序员经验分享-hwhale

我可以在“coqtop - nois”下定义策略吗？

2024-02-29 
$ coqtop -nois
Welcome to Coq 8.7.0 (October 2017)

Coq < Ltac i := idtac.
Toplevel input, characters 0-4:
> Ltac i := idtac.
> ^^^^
Error: Syntax error: illegal begin of vernac.

我正在“coqtop -nois”下重新开发“Coq.Init.Prelude”和“HoTT.Basics.Overture”以进行练习。我发现直接写表达式很难。这就是为什么我想使用战术。我想知道为什么我不能使用“Ltac”。


Ltac 现在作为插件提供，您需要加载才能使用：

Declare ML Module "ltac_plugin".
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)

coq

coqtactic

ltac

我可以在“coqtop - nois”下定义策略吗？ 的相关文章

  • Coq 中是否有一套最小完整的策略？

    我见过很多 Coq 策略 它们在功能上是相互重叠的 例如 当你在假设中得到确切的结论时 你可以使用assumption apply exact trivial 也许还有其他人 其他例子包括destruct and induction对于无感

  • Coq 中的 `destruct` 和 `case_eq` 策略有什么区别？

    我明白了destruct因为它将归纳定义分解为其构造函数 我最近看到case eq我不明白它有什么不同 1 subgoals n nat k nat m M t nat H match M find elt nat n m with Som

  • 如何在 Coq 中自动证明实数的简单相等？

    我正在寻找的是auto类似的策略可以证明简单的等式 例如 1 2 2 4 到目前为止 我手动尝试过的是使用ring simplify and field simplify来证明等式 即使这样效果也不好 Coq 8 5b3 下面的例子有效 R

  • 如何在 Coq 中将一条线的公理定义为两个点

    我想找一个例子axiom in Coq类似于几何中的线公理 如果给定两个点 则这两点之间存在一条线 我想看看如何在 Coq 中定义它 本质上选择这个简单的直线公理来看看如何定义一些非常原始的东西 因为我很难在自然语言之外定义它 具体来说 我

  • Coq：将信息保存在匹配语句中

    我正在构建一个递归函数match在清单上l 在里面cons分支我需要使用以下信息l cons a l 为了证明递归函数终止 但是 当我使用match l信息丢失 我该如何使用match保留信息 这是函数 drop and drop lemm

  • 用 Coq 重写假设，保留蕴涵

    我正在做 Coq 证明 我有P gt Q作为假设 并且 P gt Q gt Q gt P 作为引理 如何将假设转化为 Q gt P 当我尝试apply它 我只是产生新的子目标 这没有帮助 换句话说 我想从以下开始 P Prop Q Prop

  • Coq 中的程序定点和函数有什么区别？

    它们似乎有相似的目的 到目前为止我注意到的一个区别是Program Fixpoint将接受复合措施 例如 measure length l1 length l2 Function似乎拒绝这一点并且只会允许 measure length l1

  • 在 Coq 中，重写适用于 = 但不适用于 <-> (iff)

    我在证明期间有以下内容 我需要替换normal form step t with value t因为有一个已证明的定理存在等价 H1 t1 gt t1 normal form step t1 t2 tm H2 t2 gt t2 normal

  • 如何在 Coq 中禁用我的自定义符号？

    我定义了一个符号来模拟命令式编程 Notation a gt gt b b a at level 50 然而之后 所有函数应用表达式都表示为 gt gt 样式 例如 在 Coq Toplevel 的证明模式下 我可以看到 bs nat gt

  • coq 中的依赖模式匹配

    以下代码 当然不是完整的证明 尝试对依赖产品进行模式匹配 Record fail Set mkFail i nat f forall x x lt i gt nat Definition failomat forall m nat f fo

  • 在 Coq 中使用依赖类型（安全第 n 个函数）

    我正在尝试学习 Coq 但我发现很难从我读到的内容中实现飞跃软件基础 and 依赖类型的认证编程到我自己的用例 特别是 我想我应该尝试制作一个经过验证的版本nth列表上的函数 我设法写了这个 Require Import Arith Req

  • 如何暂时禁用 Coq 中的符号

    当您熟悉项目时 符号很方便 但当您刚刚开始使用代码库时 符号可能会令人困惑 我知道你可以用白话关闭所有符号Set Printing All 但是 我想保留一些打印 例如隐式参数 全部打印如下 Require Import Utf8 core

  • 将假设中的 ~exists 转换为 forall

    我陷入了假设的境地 exists k k lt n 1 f k f n 2 并希望将其转换为等效的 我希望如此 假设forall k k lt n 1 gt f k lt gt f n 2 这是一个小例子 Require Import Co

  • 逻辑：tr_rev_ Correct 的辅助引理

    在逻辑章节中 介绍了反向列表函数的尾递归版本 我们需要证明它可以正确工作 Fixpoint rev append X l1 l2 list X list X match l1 with gt l2 x l1 gt rev append l1

  • Coq - 在不丢失信息的情况下归纳函数

    当尝试对函数的结果 返回归纳类型 执行案例分析时 我在 Coq 中遇到了一些麻烦 当使用通常的策略时 比如elim induction destroy等等 信息就会丢失 我举个例子 我们首先有一个像这样的函数 Definition f n

  • 在 Coq 中查找 ++ 等定义和符号

    我们如何获得这些符号的定义 类型 例如 or of List 我努力了 Search Search Search SearchAbout and Check Check Check 然而它们都不起作用 SearchAbout 确实显示了一些

  • 在 Coq 中，“if then else”允许非布尔第一个参数？

    我读过一些教程if a then b else c代表match a with true gt b false gt c end 然而 很奇怪的是 前者不检查类型a 而后者当然确保a是一个布尔值 例如 Coq lt Check if nil

  • Coq案例分析和函数返回子集类型的重写

    我正在做一个关于使用子集类型编写经过认证的函数的简单练习 想法是先写一个前驱函数 pred forall n n nat n gt 0 m nat S m n 1 然后使用这个定义给定一个函数 pred2 forall n n nat n

  • 为什么较新的依赖类型语言没有采用 SSReflect 的方法？

    我在 Coq 的 SSReflect 扩展中发现了两个约定 它们似乎特别有用 但我还没有看到它们在较新的依赖类型语言 Lean Agda Idris 中得到广泛采用 首先 可能的谓词被表示为布尔返回函数而不是归纳定义的数据类型 默认情况下

  • 在依赖类型的函数式编程语言中，扁平化列表是否更容易？

    在 haskell 中寻找一个可以展平任意深度嵌套列表的函数时 即应用的函数concat递归并在最后一次迭代时停止 使用非嵌套列表 我注意到这需要有一个更灵活的类型系统 因为随着列表深度的变化 输入类型也会变化 确实 有几个 stackov

随机推荐

  • 使用生成的波形数据在 .NET 中播放声音

    如何根据 NET 程序根据用户输入和数学函数生成的波形数据来播放声音 我所说的 波形数据 是指固定间隔时间序列 可能是 44 1 kHz 中的 SPL 声压级 值 我认为这需要某种流缓冲区安排 请注意 这必须是现场 实时的 因此仅创建一个

  • 是否可以将通用函数分配给变量？

    func function1 arg Int gt Int return arg func function2

  • strsplit 问题 - Pig

    我有以下元组 H1 我想将其 0 拆分为元组 但是我总是收到错误消息 DUMP H1 item32 item31 1 m FOREACH H1 GENERATE STRSPLIT 0 50 ERROR 1000 解析期间出错 第 1 行第

  • 如何让notepad++在cmd中像普通记事本一样工作？

    我喜欢使用命令提示符来编写和编译java 为了编写代码 我在cmd中输入 记事本MyJavaClass java 这将打开记事本并询问我是否要创建新文件 如果它尚不存在 对我来说 问题是我喜欢使用 notepad 作为文本编辑器 因为它有很

  • 同一应用程序的多个实例在堆栈中生成

    如果有一个应用程序有登录活动 并且它通过单击图标启动 此登录活动也可以由另一个意图启动 问题是当活动运行时 通过触摸应用程序图标启动 当它收到不同的意图调用时 它会启动另一个登录活动 当收到不同的意图调用来启动登录活动时 如何在关闭当前正在

  • 在 Enum 中搜索字符串并返回 Enum

    我有一个枚举 public enum MyColours Red Green Blue Yellow Fuchsia Aqua Orange 我有一个字符串 string colour Red 我希望能够返回 MyColours Red f

  • MATLAB > MEX 文件 > 托管 DLL 中的内存泄漏

    My MEX file http en wikipedia org wiki MEX file用 C CLI 编写并调用用 C 编写的 DLL 当 gcnew 一个对象时 当 mexFunction 返回时它不应该被垃圾收集吗 它的引用应该

  • 如何使用谷歌地图 API 制作一个在特定半径范围内搜索项目的表单？

    我正在研究一个website https jsfiddle net n8aofgtz 9 embedded result我想在谷歌地图上围绕当前位置或一些手动地址画一个圆圈 用户可以选择决定是否要围绕当前位置或他们提供的某个随机地址进行环绕

  • 从 DataGridViewComboBoxColumn 选择值？

    我想知道如何选择 DataGridViewComboBoxColumn 值作为默认值 在 DataGrid 中 有 4 列以及一个 DataGridViewComboBoxColumn 数据表正在绑定网格 但对于 DataGridViewC

  • 撤消/重做实施[关闭]

    Closed 这个问题需要多问focused help closed questions 目前不接受答案 给我一些如何实现撤消 重做功能的想法 就像我们在文本编辑器中一样 我应该使用什么算法以及我可以阅读什么 谢谢 我知道撤消类型有两大类

  • 路径中的 SVG 图像 - HTML

    我遇到了一个棘手的问题 我似乎无法弄清楚 它有很多不同的文件 所以我们先不添加任何代码或文件文档 所以我得到了一个 SVG 图像 上面有很多方形路径 我在 Inkscape 中的一条方形路径上放置了一张方形图像 然后我将 SVG 文件嵌入到

  • R：使用 mouseadds lm.cluster 进行聚类稳健标准误差 - 子集和权重的误差

    我正在尝试使用 mouseadds 包中的 lm cluster 函数来获取多重插补数据集的稳健聚类标准误差 我能够运行它的标准版本 但当我尝试添加子集或权重时出现以下错误 Error in eval substitute subset d

  • .height(item.height()) jquery 在 IE 中太慢了！备择方案？

    我正在尝试设置绝对定位项目的高度以匹配其容器元素的高度 问题是这些元素有数百个 标题中的标准代码在 chrome 中运行得很好 但在 IE 中却拖得很慢 我应该如何缓解这个问题 Too SLOW in IE var starttime ne

  • 反射，从方法中获取返回值

    我们如何执行一个方法并从Reflection中获取返回值 Type serviceType Type GetType class true var service Activator CreateInstance serviceType s

  • 为什么我无法访问静态函数中的私有构造函数，如下所示？ [复制]

    这个问题在这里已经有答案了 我目前正在编写一个弱引用资源管理器 如下所示 编译器抱怨管理器有一个私有构造函数 我的问题是 为什么我无法访问静态函数中的私有成员函数 ifndef TENSOR MANAGER H define TENSOR

  • 我需要实现什么接口才能允许 VBA 中的 ForEach 作用于用 delphi 编写的 COM 对象？

    想象一下 我想在 VBA 伪代码 中执行类似的操作 并假设我有一个可枚举属性 IDList Dim MyObject object set MyObject CreateObject MyObjectClass for each Item

  • 无法安装h5py

    我正在尝试安装h5py http www h5py org 但是当我这样做时pip install h5py or use python setup py install从源代码来看 致命错误 hdf5 h No such file or

  • speex解码出错

    我使用 speex 对一些音频数据进行编码并通过 UDP 发送 然后在另一端对其进行解码 我用 speex 进行了一些测试 发现如果我在编码后立即解码数据包 则解码后的数据与原始数据相差甚远 缓冲区开头的大部分字节都是 0 因此 当我解码通

  • 任意多个节点的贝尔曼-福特距离向量算法

    我正在尝试为模拟路由器的类编写一个程序 到目前为止我已经设置了基础知识 路由器 可以通过模拟服务器向连接到该服务器的其他 路由器 发送和接收数据包 每个数据包仅包含该路由器的距离向量 当路由器接收到数据包时 它应该使用贝尔曼 福特算法相应地

  • 我可以在“coqtop - nois”下定义策略吗？

    coqtop nois Welcome to Coq 8 7 0 October 2017 Coq lt Ltac i idtac Toplevel input characters 0 4 gt Ltac i idtac gt Error

热门标签