问题标签 [idris]

像下面这样的表达式在 Idris 中是完全有效的：

有人能写出像下面这样的表达式吗？

我似乎无法编译它。

postulate是否有关于Idris 中构造的性质和用途的最新信息？教程/手册中没有任何关于该主题的内容，我似乎也无法在 wiki 中找到任何内容。TIA。

我在 idris 中有一个数据类型：

我证实它是一个具有统一性、格子、组和其他一些属性的环。

现在我想创建一个对象，它保留了我注入其中的语句的表达式。我从四个类别开始代表所有的操作，所以我得到了一个很好的语法树。例如：

这不是真正的表示，我剥离了一些需要的丑陋部分，但它给出了我试图实现的想法，上面相当于：

我认识到我可以将这些数据类型合并为一个。为了到达那里，我创建了一个函数，它将选择正确的类实例：

所以我可以保证类型中的任何东西都代表这四个操作之一：

它会抱怨：

现在我的问题是：如何确保我的数据类型中的对象经过验证并将四种不同的数据类型合二为一。我真的很想确保在施工期间这是真的。我可以理解现在解决类型类有困难，但我希望 Idris 确保它可以在构建过程中稍后完成。我怎样才能做到这一点？

代码并不是真正需要的，我对思想方向感到非常满意。

我正在尝试在 operator和 operator上对我的自定义数据类型Semigroup创建一个和VerifiedSemigroup实例：Bool&&||

所以我首先为over 运算符创建一个命名实例：Semigroup&&

但是在创建VerifiedSemigroup实例时，我如何告诉 Idris 使用 的TodosSemigroup实例Lógico？

该代码给了我以下错误：

详细说明类型时Prelude.Algebra.Main.TodosVerifiedSemigroup，方法semigroupOpIsAssociative：无法解析类型类Semigroup Lógico

我一直在尝试使用 Idris，似乎应该很简单地指定某种类型来表示两个不同数字之间的所有数字，例如NumRange 5 105 到 10 之间的所有数字的类型。我想包括双精度数/浮点数，但对整数执行相同操作的类型同样有用。我该怎么做呢？

我正在尝试完成monadLeftIdentity以下数据类型的证明：

我省略了及其对应的实例Functor，因为它们非常冗长和琐碎。让我知道，可以把它们都贴在这里。ApplicativeVerified

我试图重写return x为pure xor AllGood x，但这样做没有成功（重写对证明状态没有任何作用）。

我也尝试过这样改进return x：

但我收到以下错误消息：

怎么办？

在一些依赖类型语言（例如 Idris）中实现向量加法是相当简单的。根据维基百科上的示例：

（请注意 Idris 的整体检查器如何自动推断添加Nil和非Nil向量在逻辑上是不可能的。）

我正在尝试使用自定义向量实现在 Coq 中实现等效功能，尽管它与官方Coq 库中提供的非常相似：

当 Coq 尝试检查vpadd时，会产生以下错误：

请注意，我使用False_rect指定不可能的情况，否则整体检查不会通过。但是，由于某种原因，类型检查器无法n0与n1.

我究竟做错了什么？

大多数证明助手都是具有依赖类型的函数式编程语言。他们可以证明程序/算法。相反，我对最适合数学且仅适用于数学的证明助手感兴趣（例如微积分）。你能推荐一个吗？我听说过 Mizar，但我不喜欢源代码是封闭的，但如果它最适合数学，我会使用它。Agda 和 Idris 等新语言在多大程度上适合数学证明？

我正在与 Idris 一起工作，并且我已经为概率编写了一个类型 -Float介于0.0和之间1.0：

我希望能够将它们相乘：

我如何证明这p1 * p2将永远是一个概率？

伊德里斯版本：0.9.16

我试图描述从一个base值和一个迭代step函数生成的构造：

使用它我可以定义Plus，描述来自迭代添加jump值的构造：

简单的示例用法：

以下描述了低于 的值base是不可能的：

以下是 和 之间的base值jump + base：

我无法定义以下函数：

即：如果nis notbase加上 的自然倍数jump，则两者都不是jump + n。

如果我要求 Idris 区分大小写m，它只会显示我IBase- 然后我就卡住了。

有人会指出我正确的方向吗？

编辑 0： 申请induction给m我以下消息：

编辑 1： 名称更新，这里是源的副本：http: //lpaste.net/125873