问题标签 [idris]

我有一个带有类型签名的函数(x, y : SomeType) -> (cond x y) = True -> SomeType。当我检查 if-then-else/case/with 语句中的条件时，如何将条件为真这一事实传递给相应分支中的函数？

我正在尝试让 idris-mode 工作。我正在使用idris-dev和idris-mode的 HEAD 。每当我执行 Cl (idris-load-file) 时，我都会收到此错误

每当我尝试 Mx idris-repl 时，它都会声明Buffer *idris-repl* has no process.

该线程的结果是从 git 更新项目。但是，我使用的是每个项目的最新版本。

编辑：运行make也失败了，但这可能是一个不同的问题。如果我手动结帐0.9.16，make将通过但上述相同的问题仍然存在。

编辑：我没有在本地安装它，我是从阴谋集团沙箱中运行它的。在idris-settings.el我更改idris-interpreter-path为 idris 的完整路径。此外，当我在 emacs 之外运行 idris 时，我会收到关于找不到前奏或内置的错误。如果我添加 -i path/to/idris/libs/prelude 那么一切正常。idris-interpreter-flags但是在 in中添加“-i path/to/idris/libs/prelude”idris-settings.el并没有帮助

我想要一个Nat保持在固定范围内的。我想要功能incr，decr如果它们要将数字推到范围之外，则会失败。这似乎可能是一个很好的用例Fin，但我不确定如何使它工作。类型签名可能看起来像这样：

将Nat用于索引到Vect n. 我怎样才能实现incr和decr？Fin甚至是正确的选择吗？

有没有办法使用生成库而不是可执行文件idris？如果我尝试在没有 的情况下进行编译main，则会收到如下错误：

如果我可以生成一个库，那么有没有办法从 C 代码中调用它？我查看了生成的 C 代码，但它看起来不像是打算在外部调用。

我在 Idris 文档中没有看到正则表达式，它是否以任何（最好是可移植的）方式支持？还是计划好的？

我刚刚开始学习 Idris，我想一个不错的小项目可以开始将有限序列实现为 2-3 个手指树。树中的每个内部节点都需要在运行时使用存储在其下方的元素总数进行注释，以支持快速拆分和索引。这个大小信息也需要在编译时进行管理，以便（最终）证明用适当的索引分割和用另一个序列压缩一个序列是全部操作。

我可以想到两种方法来解决这个问题：

1. 我目前正在做的事情，只写了一小部分必要的代码：完全在类型中处理大小，然后使用类似的东西proof {intros; exact s;}来处理它们。我不知道这可能会产生什么可怕的效率后果（如果有的话）。在我心中的潜力中：a）不必要地为每个叶节点存储一个大小。b) 我认为这不太可能，但如果它坚持自下而上而不是懒惰地自上而下计算尺寸，那将是非常糟糕的。

2. 在每个节点构造函数中包含显式大小字段，以及大小字段中的数字与类型系统所需大小匹配的证明。这种方法似乎非常尴尬。从好的方面来说，我应该能够非常确定类型级别的数字和相等性证明会被删除，在运行时每个内部节点只留下一个数字。

如果有的话，哪一个是正确的方法？

当前代码

请随时提供样式提示，并可能解释如何内联尺寸代码。我只能以交互方式弄清楚要做什么，但是在底部为如此简单的事情提供证明似乎有点奇怪。

编辑

我探索过的另一个选择是尝试将数据结构与其有效性分开。这导致以下情况：

然后每个函数都附有一个（单独的）其有效性证明。

我有点喜欢这种方法将“代码”与“证明”分开的方式，但我遇到了几个问题：

1. 虽然“代码”变得更容易，但证明似乎更难构建。我想其中很大一部分可能是我不熟悉系统的结果。

2. 我实际上还没有接近编写此代码的地步，但是索引、拆分和压缩功能都必须坚持获得其输入有效性的证明。有些函数只使用序列，而另一些函数坚持证明，这似乎有点奇怪，但也许这只是我。

我有一个库项目，它需要 C 与其他语言的互操作性和合理的性能，但必须非常清楚地记录在案，比如文学编程，并且其文档可能受益于函数方法，如 Haskell，甚至是Idris的证明功能。

因此，我有兴趣将这个库构建为一个有文化的程序，首先编写文档和工作 Idris 原型代码，然后编写与 Idris 代码非常相似的 C 代码，以解决任何性能问题并轻松地与其他语言链接。

我想要什么识字的编程工具？

NuWeb是为多语言读写编程而设计的，但是它们对 @ 符号或任何转义字符的使用对于 Idris、Haskell 等函数式语言来说是有问题的。

Idris想要一个我可以贡献的有文化的编程工具。我喜欢他们只使用由块.tex分隔的文件的首选方法。\begin{code} .. \end{code}

Idris、Haskell 等不需要像 C 那样的缠结，所以这样做会增加复杂性，我希望我在这里使用的任何工具都可以保留。

为库使用者减少工具的一种方法可能是使用简单的 Perl 脚本提取 C 和 Idris 代码，例如cat_latex_env：

此时 Idris 应该可以正常编译。而且我可以嵌入 CWEB 或 NuWeb 等有文化的 C 编程工具所需的 tangle 指令。

想法？

我正在尝试使用IdrisNet2库来定义一些二进制数据结构。我正在使用 Idris 0.9.17.1 并提交 IdrisNet2 的 262b746c9a2405e43d1de6a48de44cac2fd19932。我正在定义一个带有一个 16 位字段的数据包：

我得到编译器错误：

究竟是什么问题，我该如何解决？我猜我需要向编译器证明 16 大于 0，但我不确定如何在 Idris 中执行此操作或为什么这是必要的。

我正在尝试编写一个函数，该函数mSmallest采用两个自然数作为输入n并m产生一个向量。输出向量包含具有m成员的有限集的最小n成员。

例如mSmallest 5 3应该产生[FS (FS Z), FS Z, Z]哪个是Vect 3 (Fin 5)

我想将输入参数限制m为小于n. 我试过这样的事情：

由于输入，第二种情况不应该是可能的p。我如何才能Z (S k)消除这种情况？

另外，有没有更好的方法来定义mSmallest函数？

我写了一些简单的类型来查看Vect值：

现在在我看来完全合理的是，如果我有一个Split分离向量的最后一个元素，我应该能够将它转换为SnocVect：

不幸的是，我似乎找不到任何方法来实现这个东西。特别是，我还没有找到任何方法让它让我对Split n xs参数进行模式匹配，没有它我显然无法到达任何地方。我认为基本问题是我有一些类型

并且由于++不是单射的，我需要使用某种魔法来让类型检查器相信事情是有意义的。但我对这一点理解得不够清楚，不能肯定地说。