腾讯云

文章/答案/技术大牛

发布

社区首页 >问答首页 >Coq列表排序实践& sortBy？

问Coq列表排序实践& sortBy？
EN

Stack Overflow用户

提问于 2018-07-09 04:28:06

回答 2查看 243关注 0票数 2

在Coq中，Haskell的sortBy相当于什么？

一般来说，我发现Coq标准库中围绕排序混淆。

我本来希望排序列表的一些“公理化”，以及不同类型的可用性，我可以提供一个排序函数。

然而，情况似乎并非如此。

有一个“排序列表”的理论。，它使用关系Variable R : A -> A -> Prop.，但对此R没有任何限制。我原以为这是一种命令，但不存在这样的事情。
还有一个带有"合并实施“的文件，它需要一个新的模块来传递。
没有提供像sortBy这样的帮助的“高级”版本。

我是否可以使用sortBy的某些实现，或者是否需要手动创建它？

sorting

coq

回答 2

Stack Overflow用户

回答已采纳

发布于 2018-07-09 04:47:30

Coq标准库中的MergeSort模块可以满足您的需要。它的工作方式类似于Haskell中的sortBy，除了传递一个排序函数和获得专门的排序之外，您还传递了一个封装排序函数的模块，以及该函数是完全函数的证明。参见模块文档底部的示例。

票数 3

Stack Overflow用户

发布于 2018-07-09 06:00:17

除了Coq标准库之外，图形组件库还实现了合并排序。它被称为sort，它驻留在模块mathcomp.path中。它的签名是forall T : Type, (T -> T -> bool) -> list T -> list T，它更接近于原始的sortBy。

票数 2

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/51245616

复制

【OpenDaylight】Karaf的使用

root 工具连接虚拟机主机

Xiongan-桃子

2023/06/10

9270

Kafka 删除 Apache ZooKeeper 的依赖

kafka zookeeper tcp/ip raft 存储

目前，Apache Kafka 使用 Apache ZooKeeper 来存储元数据，分区位置和主题配置之类的数据存储在 Kafka 之外一个单独的 ZooKeeper 集群中。2019 年，为了打破这种依赖关系并将元数据管理交由 Kafka，为此引入这个KIP-500 计划[1]。

smartsi

2022/01/18

1.3K0

使用apache的httpClient对异步网络请求进行封装

其他

1.对返回结果的处理进行规范 public interface INetResult<T> { void getNetData(T data) ; } 2.封装异步请求回调方法 /** * Created by gaowenfeng on 2017/8/23. * 回调类结果封装 * 实现FutureCallback接口 */ @AllArgsConstructor public class CallbackString implements FutureCallback<HttpRespo

Meet相识

2018/09/12

1.7K0

领域驱动设计对依赖的控制

架构领域驱动设计模型设计网关

我在《解构领域驱动设计》一书中分析了软件复杂度的成因，一曰规模，一曰结构，还有一个则是变化的影响。规模与结构存在一定的矛盾关系：解决规模复杂度的有效方法为“分而治之”，一旦系统被分解为多个更为细小的软件元素，结构复杂度就会增加。结构与变化之间存在互相影响的关系：如果结构控制不合理，变化带来的影响就会更强，使得系统更加复杂。

张逸

2023/03/23

4780

httpd – 对Apache的DFOREGROUND感到困惑

apache shell

所以我刚刚使用Yum在新的CentOS 7服务器上安装了Apache.我之前已经多次安装过Apache,但我从未见过这样：当我现在运行ps aux时,它总是显示出来

双面人

2019/05/31

4.4K0

Apache libcloud中对CloudStack的支持

apache

CloudStack Support in Apache libcloud 原文作者：Mark Hinkle 原文地址：https://dzone.com/articles/cloudstack-su

Steve Wang

2018/01/08

1.1K0

移除Blog对jQuery的依赖 By HKL, Tues

jquery bootstrap java javascript

1.由于博客其实动态功能并不多，而且很多都是多年前完全不懂前端的情况下写的，所以有些功能没有考虑好，现在再看了一下前端代码部分，发现很多DOM操作已经完全没有必要去用jQuery了，以后再加新功能也不会用到jQuery的特性，所以计划改写jQuery部分为原生javascript。

hiplon

2020/07/22

1.5K0

ONOS一键安装脚本

其他

工欲善其事，必先利其器。在部署SDN实践时，通常需要安装OVS和控制器等软件，经历过的同学都知道，很多时候会被一些细节卡住，影响生产效率。有时由于实验需要还需要多次部署同样的内容，重复进行多遍同样的命

SDNLAB

2018/04/03

1.4K0

OpenDaylight Carbon二次开发实用指南

linux eclipse maven ide java

通过本文你将知道： Maven Archetype的基本原理以及如何使用Maven Archetype生成适用于不同版本的ODL子项目。本文将着重讲解cli命令开发，以及Carbon Release中新引入的Blueprint的一些基本知识。OpenDaylight Carbon Release中模块运行的大致流程以及对于api和impl的开发可以参考ODL碳版本模块开发及流程梳理还有ODL controller官方开发指南（它对DataStore的描述相当不错）。如何将编写好的应用添加到一个正在运行的

SDNLAB

2018/03/29

1.4K0

Onehouse 对Apache Hudi开源社区的承诺

https 网络安全开源数据湖 apache

早些时候，我们宣布了我们的新公司 Onehouse，重磅！基于Apache Hudi的商业公司Onehouse成立，它提供了一个建立在 Apache Hudi（简称"Hudi"）之上的托管 Lakehouse 基础。在此博客中，我们的创始人兼首席执行官 Vinoth Chandar（也是 Hudi 的创建者和 PMC 主席）希望透明地宣布我们的原则和计划，以有意义且不间断的方式继续为 Hudi 社区做出贡献。

ApacheHudi

2022/04/01

6420

怎么解决网络请求的依赖关系

人工智能

怎么解决网络请求的依赖关系：当一个接口的请求需要依赖于另一个网络请求的结果思路1：操作依赖：NSOperation 操作依赖和优先级（不适用，异步网络请求并不是立刻返回，无法保证回调时再开启下一个网络请求） [operationB addDependency:operationA]; // 操作B依赖于操作思路2：逻辑判断：在上一个网络请求的响应回调中进行下一网络请求的激活（不适用，可能拿不到回调）思路3：线程同步 -- 组队列（dispatch_group） dispatch_queue_t que

陈满iOS

2018/09/10

9360

对sppnet网络的理解

编程算法

　前言：　　　接着上一篇文章提到的RCNN网络物体检测，这个网络成功的引入了CNN卷积网络来进行特征提取，但是存在一个问题，就是对需要进行特征提取图片大小有严格的限制。当时面对这种问题，rg大神采用

Gxjun

2018/03/27

7160

对sppnet网络的理解

其他

　　　接着上一篇文章提到的RCNN网络物体检测，这个网络成功的引入了CNN卷积网络来进行特征提取，但是存在一个问题，就是对需要进行特征提取图片大小有严格的限制。当时面对这种问题，rg大神采用的是对分割出的2000多个候选区域，进行切割或者缩放形变处理到固定大小，这样虽然满足了CNN对图片大小的要求，确造成图片的信息缺失或者变形，会降低图片识别的正确率. 如下图所示：

Gxjun

2018/10/09

4600

对sppnet网络的理解

其他

Gxjun

2018/10/09

5150

windows下对apache配置https协议的方法

windows apache https 数据分析 SSL 证书

windows下对apache配置https协议： 1、安装好apache环境，注意要装ssl版本的。这里装在c:/apache目录下。 2、生成服务器证书： 1）在DOS命令下进入apache/bin目录 2）在windows环境下需先设置Openssl环境变量：

用户7639835

2021/08/27

2.1K0

OpenDaylight新建HelloWorld工程并集成版本

打包

网上很多OpenDaylight的HelloWorld教程，本人就参照Lithium-SR3版本的Developers Guide （大约在17-21页），写了一个HelloWorld项目。本文对新建工程和集成到发行版的过程进行简单总结。 1、生成新的MAVEN工程。 cd ~/work/odl mvn archetype:generate -DarchetypeGroupId=org.opendaylight.controller -DarchetypeArtifactId=opendaylight-s

SDNLAB

2018/04/02

1.1K2

DLUX组件扩展下篇-实践

其他

作者： M.S-Group.皮皮熊，M.S-Group组织主要成员之一，数通行业老兵，精通传统数通网络技术，SDN/NFV新技术的狂热拥护者！

SDNLAB

2018/10/24

6230

OpenDaylight系列文章（二）：OpenDaylight初窥（上篇）之OpenDaylight的工程技术架构

ubuntu linux xml java 打包

上篇我们简单地和OpenDaylight控制器打了个照面，后续篇章会逐步介绍OpenDaylight的系统架构和实现机制。不过呢，在揭开其面纱之前熟悉它的背景技术是很有必要的。不然讨论OpenDaylight时我们就会丈二和尚——摸不着头脑。那么OpenDaylight控制器使用了哪些核心技术？它的工程技术架构又是怎样的呢？万殊一辙。OpenDaylight的工程技术架构其实就像一座高楼大厦的构造，核心技术如同风靡建筑行业的装配式技术。 OSGI---OpenDaylight的“装配式技术【画外音】

SDNLAB

2018/03/28

1.1K0

OpenDaylight系列文章（二）：OpenDaylight初窥（上篇）之OpenDaylight的工程技术架构

ODL应用开发之MD-SAL中级教程

java 编程算法 api maven 打包

1. 简介本次我们从开始设计到最终完成一个应用的开发，主要设计datastore和RPC定义和实现。Opendaylight 开发使用了OSGi框架，OSGi框架的好处在于程序设计模块化，实现紧聚合和松耦合。 Apache Karaf 是一个OSGi的容器，它可以支持部署新的应用。在OSGi里面一个bundle可能会依赖于其他的bundle。这里可能会出现一种情况，假如bundle A依赖与bundle B，bundle B 依赖于 bundle C，那么如果我们想解析bundle A，则必须解析bund

SDNLAB

2018/04/03

2.9K0

点击加载更多

相似问题

Apache Karaf -缺少依赖项(看起来像DataSources)

119

如何在Apache Karaf (Felix框架)中获取依赖链

apache karaf干净开始

没有classDeffoundError Apache Karaf

114

Apache Karaf的真正介绍

添加站长进交流群

领取专属 10元无门槛券

AI混元助手 在线答疑

关注 腾讯云开发者公众号

洞察 腾讯核心技术

剖析业界实践案例

问Coq列表排序实践& sortBy？
EN

回答 2

Stack Overflow用户

Stack Overflow用户

Apache Karaf -缺少依赖项(看起来像DataSources)

如何在Apache Karaf (Felix框架)中获取依赖链

apache karaf干净开始

没有classDeffoundError Apache Karaf

Apache Karaf的真正介绍

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问Coq列表排序实践& sortBy？EN

回答 2

Stack Overflow用户

Stack Overflow用户

Apache Karaf -缺少依赖项(看起来像DataSources)

如何在Apache Karaf (Felix框架)中获取依赖链

apache karaf干净开始

没有classDeffoundError Apache Karaf

Apache Karaf的真正介绍

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问Coq列表排序实践& sortBy？
EN