腾讯云
开发者社区
文档
建议反馈
控制台
首页
学习
活动
专区
工具
TVP
最新优惠活动
文章/答案/技术大牛
搜索
搜索
关闭
发布
登录/注册
精选内容/技术社群/优惠产品,
尽在小程序
立即前往
文章
问答
(9999+)
视频
沙龙
1
回答
Coq
中
的
记录
子
类型
,
请求
的
问题
和
参考
record
、
coq
、
subtyping
我一直在寻找在
Coq
中
讨论与
记录
相关
的
子
类型
的
参考
资料,但找不到。 我特别想知道Record _ : _ := { _ :> * }语法是什么意思,以及它是如何运行
的
。尤其是当一条
记录
有:>
和
:判断
的
混合时,我想所有的正常子
类型
关系(包括排列)都成立?请分享您认为相关
的
其他
参考
资料(键入规则、子
类型
在
Coq<
浏览 26
提问于2020-12-16
得票数 1
1
回答
Coq
:
类型
分类与从属
记录
typeclass
、
coq
我不明白
Coq
中
的
分类
记录
和
依赖
记录
之间
的
区别。
参考
手册给出了
类型
化
的
语法,但没有说明它们到底是什么以及你应该如何使用它们。一点思考
和
搜索就会发现,
类型
类本质上是依赖
的
记录
,带有一些语法糖,使
Coq
能够自动推断出一些隐含
的
实例
和
参数。当在任何给定
的
上下文中只有或多或少一个可能
浏览 1
提问于2015-04-26
得票数 10
回答已采纳
1
回答
Coq
中
的
假想命名空间
coq
、
agda
在Agda
中
,如下所示: field baz : A → A open Foo assumeFoo 该技术
的
优点是可以方便地组装
和
参数化大量
的
假设理论。在
Coq
中
,我可以将模块作为名称空间打开,并假定
记录
的
居民,但不知道如何两者兼而有之。这有可能吗?
浏览 4
提问于2017-03-30
得票数 2
回答已采纳
1
回答
Coq
的
基础
coq
我假设
Coq
会在某一时刻转向LCF方法。在过去,我对感到好奇。我在一篇总结了现有文献
的
硕士论文中找到了对Isabelle/Pure
的
一些很好
的
描述。我想知道是否有关于
Coq
内核
的
描述,涵盖了它
的
逻辑
和
实现方面。
浏览 0
提问于2020-03-06
得票数 0
1
回答
在
Coq
中
构建类层次结构?
functional-programming
、
scope
、
typeclass
、
coq
我可以使用
类型
类在
Coq
中天真地构造代数结构
的
层次结构。我在寻找有关
Coq
的
类型
类
的
语法
和
语义
的
资源时遇到了一些麻烦。然而,我相信下面是半群,么半群
和
交换么半群
的
正确实现: op_associative然而,在为AbelianMonoid构造
的
浏览 1
提问于2011-11-03
得票数 10
回答已采纳
1
回答
如何使
Coq
形式化可重用?
coq
我在研究一种算法
的
Coq
形式化。但是这个算法
的
组件(一些函数
和
引理)可以在不同
类型
上“重载”(在Haskell意义上)。 我
的
目的是避免代码重复。我知道
Coq
有模块(如ML)
和
类型
类(如Haskell)。实现引理
和
函数定义
的
可重用性
的
最佳方法是什么?它可以在不同
类型
上进行参数化?
浏览 2
提问于2015-09-30
得票数 2
回答已采纳
1
回答
Coq
:>符号
syntax
、
symbols
、
coq
这可能非常琐碎,但我在
Coq
中
找不到关于':>‘符号
的
任何信息。U:
类型
和
W :>
类型
有什么区别?
浏览 0
提问于2018-07-18
得票数 6
回答已采纳
1
回答
术语作为
Coq
中
的
类型
types
、
coq
、
term
.*)Parameter Obj: Type. Parameter
浏览 3
提问于2016-07-12
得票数 0
2
回答
COQ
中
prod
和
sig
类型
的
关系
types
、
coq
、
proof-system
在
COQ
中
,
类型
prod (具有一个构造函数对)对应于笛卡尔积,
类型
sig (具有一个构造函数)对应于依赖
和
,但是如何描述笛卡尔积是依赖
和
的
特例
的
事实?我想知道prod
和
sig之间是否有联系,例如一些定义等式,但我在
参考
手册
中
没有明确地找到它。
浏览 2
提问于2012-12-14
得票数 4
回答已采纳
1
回答
在
Coq
中
定义子
类型
关系
coq
、
subtype
有办法在
Coq
中
定义子
类型
关系吗? 我读过有关子集
类型
的
文章,其中使用谓词来确定子
类型
中
的
内容,但这不是我
的
目标。我只想定义一个理论,其中有一个
类型
(U)
和
另一个
类型
(I),它是(U)
的
子
类型
。
浏览 1
提问于2018-07-18
得票数 3
回答已采纳
1
回答
相同参数
的
模函
子
的
统一
类型
?
module
、
coq
如何让
Coq
识别出两种
类型
,每种
类型
都是从使用相同参数从模块函
子
创建
的
模块中导入
的
,但出现在不同
的
模块
中
,它们实际上是相同
的
类型
?Module Type S. End S.在上面的
Coq
文件
中
,我想声明一个公理,该公理要求G s
中
的
类型
foo与H s
中
的
类型
foo
浏览 1
提问于2020-05-25
得票数 2
回答已采纳
1
回答
不美观-打印
记录
的
字段
coq
假设我有这样
的
记录
类型
: Record myRec : Type := { myProof : myNat > 0 }.如何让
Coq
解析myRec
类型
的
值
的
字段myProof,而不是直接打印(即隐藏 它可以在声明
记录
类型
时设置吗? 或者应该使用Notation命令
和
only printing语法修饰符来完成?
浏览 14
提问于2021-10-07
得票数 2
回答已采纳
1
回答
在
coq
中
暴露归纳定义项
的
结构
lambda-calculus
、
coq
在简单
类型
的
lambda演算
中
,
类型
导
子
是唯一
的
证明在纸上是微不足道
的
。我熟悉
的
证据,通过完整
的
归纳,键入派生。但是,我很难证明
类型
派生(通过
类型
派生表示)是独一无二
的
。
Coq
给出
的
错误消息(对术语
的
抽象导致了一个错误
类型
的
术语)有点模糊,
Coq
wiki没有提供任何帮助。例
浏览 3
提问于2012-09-05
得票数 2
回答已采纳
1
回答
OCaml字符串
和
Coq
字符串(从
Coq
提取到OCaml)
ocaml
、
coq
、
coq-extraction
我使用了从
Coq
到OCaml
的
提取,其中有Z、N、positive
类型
。type positive =|
Coq
_xO of positive| N0| Z0 | Zpos of positiv
浏览 1
提问于2014-09-02
得票数 2
回答已采纳
2
回答
可以用
Coq
编写C程序吗?
coq
、
coq-extraction
我知道可以将
Coq
程序提取到Haskell
和
OCaml程序
中
。有没有办法用C来做这件事? 我正在想象一个模拟C语言
的
库。也许这样
的
库会包含一组关于C结构如何与进程内存交互
的
公理,以及关于IEEE浮点数
的
公理
和
定理。然后,它就可以在
Coq
内建立一个C程序,以及关于这个程序
的
定理。比如说,我会使用这样一个库来构建一个C快速排序算法,该算法可以在GCC可编译
的
浮点数数组上工作。
浏览 6
提问于2017-10-23
得票数 8
回答已采纳
2
回答
为什么
Coq
在将论点应用于强制性术语时不能推断出我
的
胁迫?
coq
我试图将特定西格玛
类型
的
强制写入二进制关系。强制在使用强制项作为函数参数时有效,但当使用相同
的
术语作为函数时则不起作用。下面是这个片段
的
可执行版本: 为什么第二次检查失败了?我在强制定义上犯了错误吗?还是说这是我不知道
的
胁迫推理
的
某种限制?
浏览 7
提问于2021-08-31
得票数 3
回答已采纳
1
回答
SSreflect不能与Emacs、
Coq
和
ProofGeneral一起使用。如何在MacOS
中
安装SSreflect?
emacs
、
path
、
coq
、
ssreflect
、
proof-general
如果我执行像- From mathcomp Require Import ssreflect.这样
的
操作,它会给出以下错误。这可能是因为我安装了ssreflect,但并不完全是我想要
的
方式。 但
问题
是,我想要第一种工作方式,因为我有很多程序都是用这种方式编写
的
,而且似乎不符合逻辑地更改每个程序
中
的
行。这是我
的
.emacs文件
中
的
内容-(我想我可能需要添加类似于mathcomp/ssreflect
的
路径。
浏览 15
提问于2020-03-11
得票数 0
回答已采纳
2
回答
试图“组合”相似的对象而不做大量
的
比较。
database
、
optimization
、
query
在这个数据库
中
,我有“访问权限”--每次访问都可以有任意数量(通常小于4个,有时甚至多达15个)属性。我还拥有N个用户
请求
M访问
的
“票证”,因此我有一个带有NxM“用户访问
请求
”
的
子
票表。然后,对于
子
票证,还有另一个具有访问A属性
的
表(其中"A“根据
请求
的
不同而变化)。📷 因此,例如,如果有两个用户
请求
三个访问,而这些访问分别具有2个、3个
和
4个属性,则我有1个票证<em
浏览 0
提问于2014-03-27
得票数 0
2
回答
如何查找
Coq
验证策略
的
定义或实现?
math
、
coq
、
proof
如何找到像intros或destruct这样
的
东西的确切含义,比如查找一个实现(或者如果不可能的话,一个定义)?怎样才能有效地做到这一点?
浏览 4
提问于2020-09-10
得票数 2
回答已采纳
3
回答
在vim中使用merlin在ocaml
中
开发
coq
插件
vim
、
ocaml
、
coq
、
ocamlfind
、
merlin
我安装了
Coq
与opam,并想做一个
Coq
插件。我成功地使用
coq
_makefile编译了一些插件示例,但是如果我能够在vim中使用merlin来获得
类型
信息
和
Coq
库
的
完成,那就太好了。我是否可以将
Coq
库添加到ocamlfind
中
?
浏览 9
提问于2015-04-14
得票数 5
回答已采纳
点击加载更多
扫码
添加站长 进交流群
领取专属
10元无门槛券
手把手带您无忧上云
相关
资讯
「天放AI数字人 TFGPT」21.2 在智能助理和虚拟助手行业中,使用ChatGPT可能会遇到各种类型的问题(1)
Python开源项目介绍:网站日志分析工具
干货 | 质量保障新手段,携程回归测试平台实践
深入剖析 Web 服务器与 PHP 应用的通信机制-掌握 CGI和FastCGI 协议的运行原理
MySQL数据优化总结-查询备忘录
热门
标签
更多标签
活动推荐
运营活动
广告
关闭
领券