1回答
我正在尝试定义一组描述，并将它们解释为Coq类型，这就是我到目前为止想出的： { denotesInto : D -> Type(这里需要一些文本，以便so将格式化下一个代码块:(...)但是Coq不让我这么做。在我看来，它试图解析这些调用，以表示为它找不到的其他实例，而实际上它们是对正在定义<e
浏览 9提问于2017-08-31得票数 2
2回答
在coq中使用哪个向量库？
、、、、
我想知道，在coq中是否有一个常用的向量库，即按其类型的长度索引的列表。对于那些不想使用自己的库的人来说，什么是最好的或最常见的做法？标准库中的向量我错了吗？还是人们只是
浏览 10提问于2017-02-17得票数 6
回答已采纳
我在研究一种算法的Coq形式化。但是这个算法的组件(一些函数和引理)可以在不同类型上“重载”(在Haskell意义上)。
我的目的是避免代码重复。我知道Coq有模块(如ML)和类型类(如Haskell)。实现引理和函数定义的可重用性的最佳方法是什么?它可以在不同类型上进行参数化？
浏览 2提问于2015-09-30得票数 2
回答已采纳
我想以某种方式限制构造函数在归纳定义中允许接受的输入类型。假设我想这样定义二进制数： | O : bin | S : bin -> bin.这里的思想是，D通过在末尾添加一个零来加倍一个非零数，S采用一个以零为最后一位的数字，并将最后一位转换为一。这意味着以下是合法的数字：D (S 0)而以下内容则不是：D 0
浏览 0提问于2012-12-23得票数 4
回答已采纳
2回答
对于Coq的类型，有没有一种使用递归的方法？例如，在定义show时，如果您想递归地调用列表的show函数，那么您必须使用如下所示的不动点：
Require Import Strings.String.这一切都很好，但是如果我想要定义一些用于定义Show实例的助手函数，该怎么办？就像我想要创造一个更令人眼花缭乱的节目功能，叫做magicShow，它
浏览 0提问于2018-09-15得票数 5
回答已采纳
我希望将我的程序构造成抽象模块，并编写使用抽象类型的函数。但是我不能用match来破坏抽象类型，所以我必须创建一个类似的逆引理，但是我也不能在它上match。我试着把我的问题归结为：Require Import Decidable.
Module Type decType.下面是一个例子：nat是可判定的。但其目的是编写plus等只针对抽象类型</e
浏览 0提问于2015-10-02得票数 4
回答已采纳
实际上，下面的表达式不应该编译，因为== on Trivial没有定义，充其量它应该无限期地递归。实际上，如果我对Type的理解是正确的，那么trVal1和trVal2的唯一可能类型是微不足道的。它受到类型类Eq Trivial的类型参数的约束。
浏览 3提问于2021-01-05得票数 1
回答已采纳
我正在尝试在Coq中重新实现我的一些Agda代码。我的问题是，我的一个Agda函数是由归纳谓词结构上的递归定义的。在我的Coq代码中，我试图遵循相同的风格，但有一个模式匹配限制，它不允许在Prop中分析具有类型的值的结构，从而在Set中产生结果。我的问题是:有没有一种方法可以通过递归<
浏览 2提问于2018-01-19得票数 1
回答已采纳
1回答
我想定义一个归纳类型Foo，构造函数接受一些属性作为参数。我希望这些属性依赖于我当前定义的类型的归纳参数。我希望能够使用一些接受Foo类型对象的递归函数bar从这些属性中收集一些数据。但是，我不知道有什么方法可以声明这两个，这样Coq就会接受它们的定义。我希望能够写出这样的代码： Inductive Foo : Set (* or Type *)
浏览 28提问于2020-04-27得票数 3
回答已采纳
1回答
考虑以下定点：Import ListNotations.Coq拒绝下面的不动点，因为它无法猜测递减的不动点(有时left列表会松开它的头，有时它就是right的不动点)。这个显示可以通过使用Program Fixpoint和指定{measure ((length left)+(length right))}来解决这个问题。我的问题是：
普通的Fixpoint和Prog
浏览 7提问于2017-12-14得票数 4
回答已采纳
据我所知，Coq策略是在幕后编译成一些函数式程序的，但我真的不确定这是怎么回事。我非常确定这不是我想要做的。 我想要做的是类似下面的Idris程序。prf_add_assoc' in Refl 更具体地说，我需要prf1、prf2和prf3，它们是我通过递归调用在Coq中，两个证明卡在一个lambda中，我不确定这是怎么发生的。我看到Coq<e
浏览 15提问于2019-04-09得票数 1
回答已采纳
1回答
我对Coq中的模块或类型类不是很熟悉，但根据我对它们的基本理解，我认为我有一个问题，我应该在哪里使用它们。
我想定义一个添加多态list t的所有元素的sum函数。只有当列表的元素类型(t)对plus_function和plus_id_element有一定的定义时，它才会起作用。我想写的sum的定义</
浏览 0提问于2018-02-23得票数 3
考虑以下大小列表的类型定义：| nil: forall {A: Set}, listn 0 A我试图为init定义listn函数，它删除了最后一个元素。
我尝试的实现实际上与Idris中init的定义完全相同。init : Vect (S len) elem -> Vect
浏览 6提问于2022-03-19得票数 1
回答已采纳
1回答
我不明白Coq中的分类记录和依赖记录之间的区别。参考手册给出了类型化的语法，但没有说明它们到底是什么以及你应该如何使用它们。一点思考和搜索就会发现，类型类本质上是依赖的记录，带有一些语法糖，使Coq能够自动推断出一些隐含的实例和参数。当在任何给定的上下文中只有或多或少一个可能的实例时，类型化算法似乎工作得更好，
浏览 1提问于2015-04-26得票数 10
回答已采纳
在第47页的中，定义了一个递归函数，其中每个递归步骤都使用一个格式良好的命题来表示递归终止。我无法在没有错误的情况下输入Coq。Coq抱怨在调用中递归参数不小，而教程声称是这样的。我稍微重写了代码，使其更短，但我也尝试了论文中的逐字定义
浏览 2提问于2014-11-26得票数 1
1回答
(初学者Coq问题)递归printObjItem的定义是不正确的.递归调用printJson的主体参数等于"val“，而不是"item”的子术语。
从
浏览 1提问于2019-12-04得票数 2
回答已采纳
1回答
: Set where bar : Aopen Foo assumeFoo
该技术的优点是可以方便地组装和参数化大量的假设理论在Coq中，我可以将模块作为名称空间打开，并假定记录的居民，但不知道如何两者兼而有之。这有可能吗？
浏览 4提问于2017-03-30得票数 2
回答已采纳
2回答
当我在Agda中玩弄证明验证时，我意识到我对一些类型明确地使用了归纳原理，而在其他情况下使用了模式匹配。我终于在维基百科上找到了一些关于模式匹配和归纳原则的文章：“在Agda中，依赖类型的模式匹配是语言的原语，核心语言没有模式匹配转换成的归纳/递归原则。”那么，Agda中的类型理论归纳和递归原则(在类型上定义函数)是否因为Agdas模式
浏览 20提问于2015-06-02得票数 5
2回答
我遇到了以下情况：在类的类型参数部分，当S是T的界时，类型变量T直接依赖于类型变量S；如果T直接依赖于S或T直接依赖于依赖于S的类型变量U(递归地使用此定义)，则T依赖于S。但
如果类的类型参数部分中的类型变量依赖
浏览 7提问于2017-01-24得票数 6
回答已采纳
我正在看Coq书。我试图定义一个依赖类型的函数，它返回一个长度列表，其中包含n个真，这取决于我们想要的数目。Coq抱怨说，事情没有正确的类型，但当我看到它时，如果它要展开我的定义，当做类型比较时，它应该是有效的，但它没有。为什么？Module playing_with_types2.Coq的<
浏览 15提问于2022-03-17得票数 1
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
云直播活动推荐
腾讯云开发者
