Idris是一种具有依赖类型的通用纯函数式编程语言。
1个子目标a，b：T管H：TApp a b = a ______________________________________（1/1）False（其中TApp是构造函数）在Idris中，这可以用\ Refl =>不可能证明但我没有管理......
我试图证明关于流函数和Monadic Stream函数[1]（最终是FRP程序）的属性。 Idris很满意我的流函数的形式化：模块SF导入...
无法消除名称的歧义：Idris中的Prelude.List。++，Prelude.Strings。++错误
目前我正在尝试创建一个函数，它将（a - > a - > a）的类型作为Idris中的参数，而正确的函数是idris的列表的++命令，不幸的是我得到...
假设我们希望将（带符号）整数表示为Grothendieck组的自然（或者换句话说，作为一对（m，n），其中所理解的整数是m - n）：数据ZTy：键入where。 ..
测试一个“简单”的身份类型示例，mod等同，但是传递性证明不会进行类型检查，即使是从模板中也是如此。不仅仅是修复，我想知道为什么？这是最小的片段......
我在伊德里斯做了一些开发，我遇到了以下问题。假设我们有3个向量：xs：Vect len a ys：Vect len a zs：Vect len'a并且说我们也有samelen：len = ...
我有一个依赖于谓词P：a - > Type的数据类型，这意味着它的一些数据构造函数引用具有隐式P x作为参数。我想idris能够自动推断......
我试图在Idris中编写一个zip函数，它将任意长度相同的矢量（len）组合成一个HLists矢量。也就是说，我试图概括以下功能：...
是否存在类型理论，其中相同形状的归纳数据类型的等价性是可表示的？
假设我有两个归纳定义的数据类型：归纳list1（A：类型）：类型：= | nil1：list1 A | cons1：A - > list1 A - > list1 A.和Inductive list2（A：Type）：类型：= | nil2：......
Idris Dependent Pairs：编译的程序和REPL之间的意外行为
在Idris中使用依赖对进行练习时，我在编译程序和REPL之间遇到了意想不到的行为差异。我正在测试以下数据类型：（a：...
我正在尝试在Idris中写一个2 ^ n * 2 ^ m = 2 ^（n + m）的证明。现在我有这个：expLaw :(功率2 n）*（功率2 m）=功率2（n + m）expLaw {n = Z} {m} = plusZeroRightNeutral（功率2 m）expLaw {...
假设我们正在编写一个lambda演算的实现，作为其中的一部分，我们希望能够选择一个新的非冲突名称：记录Ctx，其中构造函数MkCtx绑定：List ...
我可以在Idris中证明（s：Stream a） - >（head s :: tail s = s）吗？
以下Idris证明没有进行类型检查。 hts：（s：Stream a） - >（head s :: tail s = s）hts（x :: xs）= Refl我得到的错误是：x :: Delay xs = x :: ...之间的类型不匹配
在这个文档中，提到了如何使用替换来完成证明，但它最终使用重写，这似乎是一个语法糖，为您编写替换。我对......感兴趣 ...
在Idris中证明（x：t） - >（x == x）= True
鉴于此定义：数据LType：类型TNat：LType TFun：LType - > LType - > LType Eq LType其中（==）TNat TNat = True（==）（TFun l0 l1）（TFun r0 r1）=（l0 = = ...
我正在学习Idris，我想我会尝试为Vect类型实现Quicksort。但是我很难用实用工具方法，给定一个pivot元素和一个向量，将向量分割成......
是否有可能在简单不一致公理的结构演算中提取Sigma的第二个元素？
似乎不可能在构造微积分中提取Sigma的第二个元素。而且，似乎没有已知的，简单的方法来扩展建构的微积分......
Coq是证明助手，而Agda / Idris是编程语言（尽管它们可以称为证明助理）。我正在探索这些语言，我想知道Agda / Idris是否足以做到......
我一直在尝试使用So类型来实现SortedTwoElems证明类型和函数isSortedTwoElems。我不确定如何实现proveUnsortedTwoElems案例。这是完整的例子：......