问题标签 [idris]

我从 idris 和 idris-vim 开始。但有时会\c (IdrisCaseSplit)删除我所在的行。我尝试使用以下程序：

然后我把光标放在上面vApp并按下\d，我得到：

xs在第一种情况下，我去按\c，我得到：

到目前为止，一切都很好，但是如果我ys在第一种情况下 ( vApp [] ys) 并按\c，则整行都会被删除。

为什么行被删除？如何获得所需的行为（将 ys 替换为 []）？

如果我尝试在第二种情况下拆分 ys ，也会发生同样的事情，vApp (x :: xs) ys.

• 我在 Mac OSX、VIM 7.4 上使用 idris 0.9.14.3。
• 用病原体激活的 idris-vim。
• idris-vim 正在工作（例如，\t 工作正常）。
• :map 返回\c实际上映射到:call IdrisCaseSplit()<CR>
• 我已经尝试过使用最小的 vimrc，以避免任何干扰。

提前致谢。

注意： 这似乎是 idris 本身的错误？

我一直在研究依赖类型，我了解以下内容：

1. 为什么全称量化被表示为依赖函数类型。∀(x:A).B(x)意思是“对于所有x类型A，都有一个类型的值B(x)”。因此，它被表示为一个函数，当给定任何x类型的值时，它返回一个类型的A值B(x)。
2. 为什么存在量化被表示为依赖对类型。∃(x:A).B(x)意思是“存在一个x类型的类型A，它有一个类型的值B(x)”。因此，它表示为一对，其第一个元素是type的特定值，其第二个元素是 type 的值。xAB(x)

旁白：有趣的是，普遍量化总是与物质暗示一起使用，而存在量化总是与逻辑连词一起使用。

无论如何，关于依赖类型的维基百科文章指出：

依赖类型的对立面是依赖对类型、依赖总和类型或sigma-type。它类似于联积或不相交的联合。

对类型（通常是乘积类型）如何类似于不相交的联合（总和类型）？这一直让我感到困惑。

此外，依赖函数类型与产品类型有何相似之处？

为什么 Idris 要求函数按照它们的定义和相互递归的顺序出现mutual？

我希望 Idris 在函数之间执行第一次依赖分析，并自动重新排序它们。我一直相信 Haskell 可以做到这一点。为什么这在伊德里斯是不可能的？

如何使用 Idris FFI 调用具有 FPtr 类型的 NULL 参数的函数？我浏览了这个库，看起来既没有空指针，也没有将整数转换为指针的方法。

Type 1一个既不是Type也不是 的居民的例子是Type什么？在 Idris REPL 中探索时，我无法提出任何建议。

更准确地说，我正在寻找x其他一些Type产生以下结果：

我正在尝试制作一个 Idris 类型的函数(j : Nat) -> {auto p : So (j < n)} -> Fin n来将 a 转换Nat为 a Fin n。为了使Z案例起作用（和输出FZ），我试图证明证明0 < n足以使FZ : Fin n. 但我无法弄清楚如何做到这一点。

我愿意制作一个完全不同的函数，只要它可以将Nat值转换为Fin n值（它们存在的地方）。我的目标是拥有一些可以将任何Nat转换为Mod n​​值的其他函数，例如，15 : Nat映射到3 : Mod 4. 我的Mod类型目前有一个构造函数，mkMod : Fin n -> Mod n.

例如，可以在 Idris 中的函数中返回类型

但是出现了我想用来->折叠类型列表的情况（在尝试编写一些解析器时），即

所以那typeFold [String, Int]会给String -> Int : Type. 虽然这不会编译：

但这很好用：

有没有更好的使用方法->，如果没有，是否值得作为功能请求提出？

I'm trying to make what one might call a decidable parser in Idris. At first I am just looking at parsing natural numbers, but have ran into an unexpected problem. A minimum example of the code that produces it is this:

I would expect this to compile, but instead I get

But natToChar 0 clearly equals '0', so I don't understand what the problem here is.

Update

I have also asked a question more directly related to what I am trying to do here.

我正在使用这种类型来推断可以执行可判定解析的字符串：

例如，像这样定义数字 [0-9]：

那么我们可以有以下功能：

这个s2n函数现在可以在编译时正常工作，但它本身并不是很有用。要在运行时使用它，我们必须先构造证明Every Digit (unpack s)，然后才能使用该函数。

所以我想我现在想写这样的函数：

或者我们想要返回成员资格证明或非成员资格证明，但我不完全确定如何以一般方式执行这些操作。因此，我尝试Maybe只为字符制作版本：

但后来我得到这个统一错误：

但p 属于类型Char -> Type。我不确定是什么导致了这个统一失败，但认为这个问题可能与我之前的问题有关。

这是我想要做的事情的明智方法吗？我觉得目前的工作有点多，这些功能的更通用版本应该是可能的。auto如果关键字可以用于编写一个函数给你一个Maybe proof或一个，这将是很好的Either proof proofThatItIsNot，就像DecEq类的工作方式一样。

我正在尝试通过重建（以更简单的方式）我们最近在工作中所做的一些东西来学习 Idris。

我想要一种数据类型，它可以用贷方向量和借方向量对总账进行建模。我已经做到了这一点：

但我不确定如何将记录添加到已经存在的 GL。

具有类似的功能

我如何检查/强制执行新 GL 是否遵守规则？