我希望创建一类可以证明某个元素为正或负或为零的类型。我已经创建了一个接口: interface Signed t where data Negative : t -> typewhere data IsZero : Nat -> Type
ZZero : IsZero Z 在实现中那么,如何在接口中实现类型呢?那么
是否有可能为Idris中的接口创建可判定的属性,这些属性可以在接口本身中使用?例如,假设我们有一个简单的接口Foo和一个数据类型FooTypeEmpty,表示给定foo对象是‘空’的语句(定义为‘由两个零索引’):isEmpty : (f : foo n m a) -> Dec (FooTypeEmpt
在另一个问题()中,我不得不试图理解为什么Prelude.Applicative.guard需要Ord类型。保护被定义为guard a = if a then pure () else empty
看看Alternative接口 (我实际上还不明白它是如何在代码中定义的,但我在学习Idris方面还没有太远),我也不认为它需要Ord。