具有相同索引的归纳类型的两个值的模式匹配

文章/答案/技术大牛

发布

0回答

pattern-matching、coq、dependent-type

为什么以下代码不进行类型检查(coq-8.5pl3)？模式匹配似乎忘记了u和v具有相同的类型。

浏览 0提问于2017-06-13得票数 1

回答已采纳

1回答

我可以在立方Agda中使用归纳类型族吗？

agda、homotopy-type-theory、cubical-type-theory

我注意到立方标准库将Fin定义为依赖对，而不是索引归纳类型。原因是Cubical Agda不完全支持索引归纳类型：https://github.com/agda/cubical/pull/104#discussion_r268476220 一个相关的问题指出，模式匹配不适用于归纳家族，并编写了一个模式匹配函数，它似乎工作得

浏览 15提问于2020-01-28得票数 6

回答已采纳

2回答

Agda中基于归纳原理的函数定义

agda、type-theory

当我在Agda中玩弄证明验证时，我意识到我对一些类型明确地使用了归纳原理，而在其他情况下使用了模式匹配。我终于在维基百科上找到了一些关于模式匹配和归纳原则的文章：“在Agda中，依赖类型的模式匹配是语言的原语，核心语言没有模式匹配转换成的归纳/递归原则。”那么，Agda中的<

浏览 20提问于2015-06-02得票数 5

1回答

在Coq中为共归纳类型流定义一个“head”(没有模式匹配)

coq、coinduction

( 1)我认为在不进行模式匹配的情况下，可以使用归纳类型。(仅使用_rec、_rect、_ind )。它是不透明的，复杂的，但可能的。( 2)是否有可能使用具有模式匹配的共进类型？从共归纳型到同归纳型构造子域的结合都存在着一个函数。Coq是否显式地生成它？如果是，如何重写“hd”？ Section stream

浏览 2提问于2016-11-25得票数 1

回答已采纳

1回答

在Coq中，“如果是”允许非布尔的第一个参数？

if-statement、types、coq

但是，前者非常奇怪地不检查a的类型，而后者当然确保a是一个布尔值。为什么if ... then ... else ...允许它的第一个参数不是一个非布尔值？是否存在过载？(Locate "if".没有给出结果。)

浏览 1提问于2017-12-25得票数 4

回答已采纳

1回答

在这个例子中Coq的类型系统是做什么的？

coq

我对Coq类型系统在下面h的定义中证明术语的匹配部分的行为感到困惑：由于H的类型为x= y，因此由于return子句，匹配项将返回一个类型为b=y -> b=x的项。在应用了下面的各种术语之后，我们得到了h的预期<em

浏览 3提问于2017-07-27得票数 4

回答已采纳

1回答

在Coq中通过归纳谓词上的递归定义函数

coq

我正在尝试在Coq中重新实现我的一些Agda代码。我的问题是，我的一个Agda函数是由归纳谓词结构上的递归定义的。在我的Coq代码中，我试图遵循相同的风格，但有一个模式匹配限制，它不允许在Prop中分析具有类型的值的结构，从而在Set中产生结果。我的问题是:有没有一种方法可以通过递归在证明上定

浏览 2提问于2018-01-19得票数 1

回答已采纳

1回答

Raft如何保证日志一致性？

algorithm、distributed-computing、distributed-system、raft

我正在学习木排，我已经知道木排的基本原理。在匹配的<entry, term>之前，Raft如何保证领导者和追随者的日志是相同的？

浏览 0提问于2020-01-21得票数 0

1回答

参数不同，但函数的行为是相同的

coq

Abort. deriveP_eq成立，而updateRnP只是deriveP的递归。所以我认为RnP_eq必须坚持住。但是，我不知道如何证明这一点。我需要在n或p中进行归纳，但这会改变函数J的类型，并且我不能将归纳假设应用于目标。用Coq证明RnP_eq是不可能的吗？ Require Import Psatz.

浏览 19提问于2020-10-26得票数 1

回答已采纳

1回答

基于效果的通用程序设计

haskell、generic-programming、agda、dependent-type、idris

Effect : Type如果我们允许资源为值并交换前两个参数，我们将得到(其余代码在Agda中)(例如lambda抽象(Lam)构造函数类型(σ ⇒ τ) (为了便于描述，我将忽略索引也包含类型之外的上下文)，r表示许多归纳位置(Var不(⊥)接收任何TermE，Lam接收一个TermE (⊤)，App接收两个(Bool)

浏览 4提问于2016-01-22得票数 20

回答已采纳

1回答

Coq可以做什么，而Agda/Idris不能做？

coq、agda、idris

我正在探索这些语言，我想知道Agda/Idris是否足以做Coq所能做的一切。那么，有没有一些证据/管理代码/IDE (Emacs)函数的方法/其他Coq可以做而Agda/Idris不能做的事情呢？

浏览 21提问于2017-12-16得票数 9

回答已采纳

3回答

为什么打字是件坏事？

agda、dependent-type、idris

Agda和Idris都有效地禁止了Type类型值的模式匹配。看起来Agda总是在第一种情况下匹配，而Idris只是抛出一个错误。那么，为什么打字是件坏事？它会破坏一致性吗？我还没有找到很多关于这个话题的信息。

浏览 8提问于2014-04-22得票数 50

回答已采纳

2回答

具有相同类型的两个值的依赖模式匹配

pattern-matching、coq、dependent-type、convoy-pattern

让我们假设我们有一些P : forall {m : nat} (x y : fin m) : Set (重要的是P的两个参数都是相同类型的)。*)因此，也许我们可以使用相等的证明来强制转换x，其类型与y相同。然而，它并没有任何有用的价值。例如，下面将生成一个具有五个嵌套<e

浏览 4提问于2017-07-23得票数 1

回答已采纳

1回答

Agda中的参数化诱导型

gadt、agda

在参数化类型的介绍中，作者提到了在本声明中 [] : List AList的类型是Set → Set，而A成为两个构造函数的隐式参数，即。where _::_ : {A : Set} → A → List A → List A 遗憾的是，这不起作用(我试着学习两天左右的</

浏览 1提问于2012-01-22得票数 15

回答已采纳

1回答

SML匹配表达式中的模式是否应该具有相同的类型？

functional-programming、pattern-matching、programming-languages、sml、ml

在Ullman的SML书中：=><pattern 1> => <expression 1> <pattern2> => <Expression2> => =‘>后面的每个表达式都必须是相同的类型，因为它们中的任何一个都可能成为匹配的</e

浏览 0提问于2020-04-30得票数 0

回答已采纳

2回答

为什么J公理在给出x，y的签名时取2 x？

equality、agda、type-theory

首先，我已经查阅了一些相关的材料，包括HoTT书& 。J : forall {A : Set} {C : (x y : A) → (x ≡ y) → Set} →J c x x refl = c x ，(唯一的区别是我去掉了点符号)？或者说，为什么第二个x是用x而不是y写的呢

浏览 2提问于2018-10-16得票数 4

回答已采纳

3回答

模式匹配数组

ocaml

我有一个函数，返回数组的最小值。该函数的类型如下：它的实施是： | [] -> 1000000000 | x :: []那么，我如何才能与数组匹配呢？

浏览 2提问于2016-10-26得票数 3

回答已采纳

2回答

Elasticsearch类型与不同模式的索引

elasticsearch

什么是类型？但是，在中，它仍然提到我们需要将

浏览 6提问于2016-10-14得票数 0

回答已采纳

2回答

在Coq (安全nth函数)中使用依赖类型

coq

我正在努力学习Coq，但我发现很难从我在软件基础和依赖类型的认证编程到我自己的用例中所读到的东西实现飞跃。如何从其他代码调用此函数，即如何提供所需的证明？部分编写什么之前，这是行不通的。我试着把

浏览 1提问于2014-12-24得票数 4

回答已采纳

1回答

(true=true)的所有证明都一样吗？

coq

也就是说，true = true的所有证明都是相同的？最好不用添加任何公理(比如UIP)。我发现了以下线索，表明情况可能是这样的：

浏览 0提问于2018-06-13得票数 3

回答已采纳

点击加载更多