问题标签 [convoy-pattern]

问问题

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

11 问题
Newest
Active
Bountied
318
Unanswered
0 投票
1 回答
53 浏览

coq - 当我知道磁头不会失败时，我可以避免使用选项 A 吗？

我在 ATP 的世界里还是个新手，但肯定很有动力。我开始处理依赖类型。我参与了一个项目，我在其中定义了（有限和无限）序列的类型。

现在我想定义一个非空序列的头部。

我的问题在于 Hd 的定义：我不知道如何证明@hd_error A l = None，因为我们已经在这样的匹配分支中。我相信这应该很容易。

我在最后一个定义中有一个类似的问题，因为我不知道如何转换 H，对于第一个匹配分支的特殊情况，我知道这一点length s = Datatypes.length x，因此0 << length s -> 0 < Datatypes.length x.

最后，我省略了关于 << 和长度序列的细节，因为我认为它与问题无关，但基本上我已经用 Inf 提升了 nat 来表示无限序列的长度，而 << 是 nat 的 < 和编号。

我已经学习了软件基础课程，我目前正在学习更多使用“具有依赖类型的认证编程”，这也非常好。在此先感谢，米格尔


12345678910