idris 相关问题

Idris是一种具有依赖类型的通用纯函数式编程语言。

如何从Idris中的fastPack获取正常值?

我对 Idris2 中 pack 和 fastPack 函数之间的区别感到困惑(从 0.7.0 开始)。两者具有相同的签名: :t 包 Prelude.pack:列表字符 -> 字符串 :t 快速包 前奏.fastP...

回答 1 投票 0

删除类型构造函数中的参数

删除类型构造函数中的参数是什么意思?例如 数据 Foo : (0 _ : Nat) -> 输入其中 相对于 data Foo : Nat -> 输入其中 我的理解是

回答 1 投票 0

在Idris2中导入目录是什么意思?

我通常会看到 Idris 中的导入指令用在 .idr 文件上。但在此处的代码中,我看到在目录上使用了导入实例。 导入公共 Text.Lexer ,其中 Text.Lexer 是一个目录

回答 1 投票 0

如果证明是正交的有帮助吗?

假设我有一个函数 f : Vect m Nat -> Vect n Nat -> {auto _ : 证明 m n} -> Foo m n 在哪里 数据证明:Nat -> Nat -> 输入其中 等式:证明 x x 一:证明1_ 我可以做一个

回答 1 投票 0

了解 Idris 中的依赖类型机器

我试图遵循这本书中自动售货机的示例。因此,沿着门示例的脚步,我想用更简单版本的门来复制相同的场景......

回答 1 投票 0

无法匹配两个相同的类型

我真的不知道如何正确解决这个问题,因为我是伊德里斯的新手,所以我会讲我的故事。 我正在实现一个类型安全的 sprintf 函数,具有以下类型签名: sprintf : (s: Str...

回答 1 投票 0

Idris 依赖记录,对类型构造函数参数具有接口约束

是否可以对 idris 中依赖记录的类型构造函数的参数进行接口约束? 假设我有一个界面 Show : Type -> Type。现在我需要限制...

回答 2 投票 0

Idris:重写不起作用(重写者...没有改变)

我正在证明 Idris 中的一个定理,在第二种情况下: 定理1 t1 t2 s (S_Trans u hyp1 hyp2) = 让 (s1 ** (s2 ** (ueq, st1, st2))) = 定理1 t1 t2 u hyp1' = 在 hyp1 中重写 ueq 万一

回答 1 投票 0

idris2中的mapM和mapM_相当于什么?

我知道有一个 mapM 函数,它将一元操作应用于列表并返回一个包含列表的一元值。 (参见例如 Haskell中的mapM_和mapM有什么区别?) 但我

回答 2 投票 0

idris 是否支持一种将对称语句折叠成一个的方法?

我是函数式编程的新手,因此正在学习“使用 Idris 进行类型驱动开发”。 给出一个函数 maxMaybe ,它可以计算两个 Maybe Double 之间的最大值,定义如下 最大也许:...

回答 2 投票 0

在 Idris 2 中选择命名实现

根据这个旧答案,Idris 1 使用 using 语法来选择代码块的默认实现。对应的 Idris 2 语法是什么? 我尝试过使用答案中的语法...

回答 1 投票 0

如何使用依赖对的结果?

我正在 idris 中学习依赖对,但不明白如何使用它。例如,如果我过滤 Data.List,我会返回一个 Data.List,您可以对其进行求和或其他计算。 总和 $ f...

回答 1 投票 0

具有单子效果的流类型

是否有 Stream 类型的标准类型(特别是在 stdlib 中)(我指的是潜在的无限惰性序列),它允许在访问下一个元素时产生效果?有点像...

回答 0 投票 0

builddir 和 outputdir 是什么,为什么它们会生成“未找到文件”错误?

目标:在 Idris2 中打包一个可执行的“Hello, world”程序 我正在研究文档,它提供了包字段的描述,但遗憾的是没有提供任何示例。 问题...

回答 0 投票 0

关于在Haskell类语言中通过部分应用定义 "多变量 "函数的问题

所以,我实际上是在修整Idris语言,有点按照Brady的Idris类型驱动开发。我不认为我在这里写的东西与特定的编程语言有什么联系(......)。

回答 1 投票 4

Idris函数出现类型不匹配的错误

我是Idris的新手。我正在研究以下函数average : String -> Double average str = let numWords = wordCount str totalLength = sum (allLengths (words str))in ...。

回答 1 投票 0

如何选择运算符优先级?

在Idris中,您可以使用infix,infixl或infixr定义运算符,其后是运算符的优先级,然后是一系列运算符,例如infixl 8 +,-我想您可以在其他...中进行此操作]]

回答 1 投票 1

重新连接自己的Vect但遇到问题

我试图重新实现Vect数据类型以更加熟悉相关类型。这就是我写的:data Vect:(len:Nat)->(elem:Type)->类型,其中Nil:Vect Z ...

回答 1 投票 2

Idris:Ord / Num问题

我有一个非常简单的示例,作为该示例的使用案例_的演示,它没有类型检查,而且我无法理解问题所在:数据ZeroOrSign = Zero |位置|负号:Ord ...

回答 1 投票 1

为什么这个函数/构造函数参数成为一个自由的隐式变量?

[我正在尝试在Idris中实现Agda的检查习惯,作为解决此问题的可能方法,但是,当我在MkReveal构造函数上进行模式匹配时,似乎丢失了f的选择,并且...]]

回答 1 投票 0

© www.soinside.com 2019 - 2024. All rights reserved.