idris

4热度

1回答

我正在学习伊德里斯，作为一项个人练习，我想实现一个由所有素数组成的Primes类型。 idris中有一种方法来定义一个从类型和属性开始的新类型，它将选择属性为true的所有启动类型的元素？在我的情况下，有没有办法将Primes定义为Nat这样的集合，使得n <= p and n|p => n=1 or n=p？如果这是不可能的，我应该使用某种筛子定义素数来构建它们吗？

1热度

1回答

伊德里斯类型导出用于算术运算

在下面的代码 Idris> :t \x => x + x \x => x + x : Integer -> Integer 伊德里斯导出一个整数类型的X变量，其中我认为它应该得到像在Haskell接口不限于： Haskell> :t (\x y -> x + y) (\x y -> x + y) :: Num a => a -> a -> a 然后它甚至不像一个Integer，接受Do

5热度

2回答

如何限制输入类型和输出类型相同？

我正在通过Manning的Idris类型驱动开发。给出了一个例子，教导如何将函数限制在一个类型族中的给定类型。我们有Vehicle类型，它使用PowerSource，即Pedal或Petrol，我们需要编写一个函数refill，该类型只适用于使用汽油作为能源的车辆。以下代码有效，但不能保证填充Car将生成Car而不是Bus。我如何需要将refill函数的签名更改为只允许在给出Car时生成Car并

0热度

1回答

如何在Idris中编写Vect的正确类型签名？

最近我一直在探索Idris中的依赖类型。然而，我克服了一个非常烦人的问题，这是在伊德里斯，我应该用类型签名开始我的程序。所以问题是，如何在Idris中编写简洁的类型签名？例如， get_member : (store : Vect n String) -> (idx : List (Fin n)) -> (m : Nat ** Vect m (Nat, String)) get_member

0热度

1回答

光年解析器的行为在意想不到的方式

我试图建立与伊德里斯一光年格式化。整个项目到目前为止是在这里： https://github.com/hejfelix/IdrisFMT/blob/501a4a9e8b1b4154ed0d7836676c24d98de8b76a/IdrisFmt.idr 现在，目的是来标记文件本身，然后漂亮的打印出来，即文件作为输入应该是一个固定点。这个问题是每个字符串文字，我的解析器似乎吃了空白之后。如果在

4热度

2回答

为什么基于相关对的过滤器？

在Idris Tutorial中，用于过滤矢量的函数是基于相关对的。 filter : (a -> Bool) -> Vect n a -> (p ** Vect p a) filter f [] = (_ ** []) filter f (x :: xs) with (filter f xs) | (_ ** xs') = if (f x) then (_ ** x :: xs')

7热度

3回答

相关类型：矢量矢量

我是新的依赖类型（尽管它们之间存在很大的差异，但我仍然试图使用Idris和Coq）。我试图表达以下类型：给出一个类型T和一个k nats，n2，... nk序列，这个类型由k个长度为n1，n2的T序列组成。。nk分别为。也就是说，一个矢量的矢量，其长度由参数给出。这可能吗？

2热度

1回答

汇总和搜索流中的元素

我想要一个find函数用于大小有界类型的流，类似于列表和查找函数。 total find : MaxBound a => (a -> Bool) -> Stream a -> Maybe a 的挑战是它，使其：是总消耗不超过恒定 log_2Ñ空间，其中N是编码最大a所需的比特的数量。时间不超过一分钟，以检查在编译时没有征收成本运行通常对于流的总能找得到实现听起来荒谬。流是无限的，

3热度

1回答

Idris中有理数的实现

Idris中有理数的实现是否存在？ E.g.来自Haskell的Data.Ratio端口。

2热度

1回答

LTE整数（ZZ）

我是（为了好玩吗？）试图通过所有如何证明它在伊德里斯工作。我将要求的其中一个属性是整数的总排序。伊德里斯已经有了提供基于感应的整数的模块data.ZZ。我需要添加一个类似于Nat的LTE的类型。我似乎无法说服我自己，我的实施是正确的（或者说LTE是正确的）。如何“检查”我正在处理的LTEZZ数据类型是否有效？如何检查(LTE 4 3)无效？示例代码如下：所有的 %default total |