枚举类型的Idris - Eq
枚举类型是一种数据类型，它用于定义一个有限的值集合。在编程中，枚举类型通常用于表示一组相关的常量。Idris是一种依赖类型的编程语言，它支持枚举类型的定义和使用。
在Idris中，可以使用data关键字来定义枚举类型。例如，我们可以定义一个表示颜色的枚举类型：
data Color : Type where
Red : Color
Green : Color
Blue : Color在上述代码中，Color是一个枚举类型，它有三个可能的值：Red、Green和Blue。我们可以使用这些值来表示不同的颜色。
枚举类型在编程中有许多优势。首先，它可以提高代码的可读性，因为它明确地列出了可能的取值。其次，枚举类型可以帮助我们在编译时捕获一些错误，例如使用了未定义的枚举值。此外，枚举类型还可以用于模式匹配，使得代码编写更加简洁和易于维护。
在云计算领域，枚举类型可以用于表示不同的资源类型、状态或配置选项。例如，我们可以使用枚举类型来表示虚拟机的不同规格、存储类型的选择、网络安全策略等。
腾讯云提供了丰富的云计算产品和服务，其中一些与枚举类型相关。例如，腾讯云的云服务器（CVM）提供了不同的实例规格供用户选择，用户可以根据自己的需求选择适合的规格。腾讯云的对象存储（COS）提供了不同的存储类型，包括标准存储、低频存储和归档存储，用户可以根据数据的访问频率和成本要求选择适当的存储类型。
更多关于腾讯云产品的信息可以在腾讯云官方网站上找到：
相关·内容
Idris具有非常简单的cong函数。
cong : {f : t -> u} -> a = b -> f a = f b
cong Refl = Refl
如果我为超过零的加法创建一个特殊形式的cong，它不能进行类型检查。
cong0 : {f : Nat -> Nat} -> a + Z = a -> f (a + Z) = f a
cong0 Refl = Refl
在Idris 1中，我得到了
When checking left hand side of cong0:
When checking an application of Main.co
浏览 14提问于2021-05-21得票数 1
我想知道如何证明(So (not (y == y)))是Uninhabited的一个实例，但我不确定该怎么做。它在Idris中是可证明的，还是由于y的一个奇怪的Eq实现的可能性而不可证明？
浏览 13提问于2017-07-02得票数 3
回答已采纳
当我在Idris解释器中输入这个简单表达式时，它会导致一个错误：
Idris> (\x=>2.0*x) `map` [1..10]
When checking an application of function Prelude.Functor.map:
Can't find implementation for Enum Double
到底是怎么回事？
我认为这是可行的，因为List Int将映射到List Double中，因为映射类型允许不保留原始类型。
浏览 1提问于2018-04-17得票数 2
回答已采纳
1回答
平等模式匹配
、、
我对伊德里斯有点陌生。我以前用过一点agda，我在GHC Haskell有很强的背景。我试着去理解为什么在GHC Haskell中工作的东西在Idris不起作用。以下代码未编译(idris版本0.12.3，nobuiltins，noprelude)：
data Nat = S Nat | Z
plus : Nat -> Nat -> Nat
plus Z right = right
plus (S left) right = S (plus left right)
rightIdentityAlt : (n : Nat) -> n = (plus n Z)
浏览 1提问于2018-01-19得票数 11
回答已采纳
当我有一个"enum“类型，即没有任何情况包装任何其他数据的代数数据类型时，我通常喜欢将解析器/打印机从映射映射到字符串，以确保解析器和打印机在我更改代码时保持同步。例如，在Idris：
data RPS = Rock | Paper | Scissors
Eq RPS where
Rock == Rock = True
Paper == Paper = True
Scissors == Scissors = True
_ == _ = False
StrMap : List (RPS, String)
StrMap =
[ (Rock, "rock&#
浏览 1提问于2018-12-06得票数 1
1回答
我正在尝试证明有关流函数和一元流函数1的性质。 Idris对我的流函数形式化很满意： module SF
import Data.Vect
import Syntax.PreorderReasoning
%default total
data SF : Type -> Type -> Type where
SFG : (a -> (b, Inf (SF a b))) -> SF a b
steps : {n : Nat} -> SF a b -> Vect n a -> Vect n b
steps {n = Z} (SFG s) [
浏览 19提问于2019-04-02得票数 1
2回答
我试图比较String和String，期待True。
Idris> String == String
Can't find implementation for Eq Type
然后，当我将一个False与一个Bool进行比较时，我期望得到Bool。
Idris> String /= Bool
Can't find implementation for Eq Type
我是不是错过了一个import
浏览 2提问于2016-04-11得票数 6
回答已采纳
我正在努力提高我的Idris技能，通过查看一些练习 (最初是为Coq，但我希望翻译到Idris不太坏)。我在上遇到了麻烦，它写着：
删除“承认”然后填上证据。
定理plus_id_exercise：∀nat: nat，n=m→m=o→n+m=m+ o.证明。(*填写这里*)承认。
我已翻译成Idris中的下列问题：
plusIdExercise : (n : Nat) ->
(m : Nat) ->
(o : Nat) ->
(n == m) = True ->
浏览 3提问于2018-05-26得票数 2
回答已采纳
1回答
我试图用Idris编写一个记录，但是它有一个泛型参数，需要受到接口的约束。对于正常的联合类型，我可以写：
data BSTree : (a : Type) -> Type where
Empty : Ord a => BSTree a
Node : Ord a => BSTree a -> a -> BSTree a
但我正试图找出做同样事情的语法，只是记录一下。我试过这样的方法：
record Point a where
constructor MkPoint : Eq a => a -> a -> Point a
x : a
浏览 0提问于2017-07-17得票数 2
回答已采纳
2回答
使用Idris的类型驱动开发展示了这个练习：
same_cons : {xs : List a} -> {ys : List a} -> xs = ys -> x :: xs = x :: ys
但是，我尝试通过以下方式实现它：
data EqList : (xs : List a) -> (ys : List a) -> Type where
Same : (xs: List a) -> EqList xs xs
sameS : (xs : List a) -> (ys : List a) -> (x: a) -> (eq : E
浏览 0提问于2016-05-06得票数 0
我只是想把下面的Haskell翻译成Idris (我不是在寻找效率或正确性的证明)：
quicksort [] = []
quicksort (x:xs) = quicksort [y | y <- xs, y<x ]
++ [x]
++ quicksort [y | y <- xs, y>=x]
下面是我的Idris代码，除了需要告诉Idris我们所处理的是有序类型之外，它基本上与Haskell一样：
quicksort: List
浏览 0提问于2018-05-08得票数 2
回答已采纳
1回答
在Idris中，字符串是原语，而不是Haskell中的列表。因此，我希望有某种原始的replace : (needle : String) -> (replacement : String) -> (haystack : String) -> String函数-- la 。我一直找不到这个。但我想，也许我能找到一些replace : Eq a => (needle : List a) -> (replacement : List a) -> (haystack : List a) -> List a函数a la ，因为Idris确实提供了unpack
浏览 0提问于2018-07-25得票数 2
回答已采纳
1回答
我是新的Idris和一般的证明，但我正在通过软件基础移植到Idris。我正在做一项练习
namespace Booleans
data Bool = True | False
andb : Booleans.Bool -> Booleans.Bool -> Booleans.Bool
andb True b = b
andb False _ = False
orb : Booleans.Bool -> Booleans.Bool -> Booleans.Bool
orb True _ = True
orb False b = b
浏览 0提问于2019-09-05得票数 0
回答已采纳
考虑以下大小列表的类型定义：
Inductive listn: nat -> Type -> Type :=
| nil: forall {A: Set}, listn 0 A
| cons: forall {n: nat} {A: Set}, A -> listn n A -> listn (S n) A.
这本质上是Idris中的类型。
我试图为init定义listn函数，它删除了最后一个元素。
我尝试的实现实际上与Idris中init的定义完全相同。这是在伊德里斯：
init : Vect (S len) elem -> Vect len elem
init
浏览 6提问于2022-03-19得票数 1
回答已采纳
1回答
我正试图在Idris中实现，作为的一种可能的解决办法，但是，当我在MkReveal构造函数上进行模式匹配时，f的选择似乎丢失了，反而变成了一个自由参数。
首先，inspect的Idris端口
%default total
data Reveal : {a : Type} -> {b : a -> Type} -> (f : (x : a) -> b x) -> (x : a) -> (y : b x) -> Type where
MkReveal : {a : Type} -> {b : a -> Type} -> {f : (
浏览 2提问于2020-05-21得票数 0
回答已采纳
TL;DR:我想举一两个在Idris中使用来帮助我更好地理解它的例子。
泛型相等类型的概念定义如下：
data (=) : a -> b -> Type where
Refl : x = x
当我第一次遇到这种情况时，我对语法感到非常困惑。(我一直认为=是一种运算符，而不是类型。)但是在REPL里玩它让我明白了。例如，我们可以声明类型来表示假等式：
λ> 2 + 2 = 5
4 = 5 : Type
λ> 2 = "wombat"
2 = "wombat" : Type
但是，=的唯一构造函数是Refl，只有在两个参数相等时才能使用它
浏览 1提问于2019-05-05得票数 1
回答已采纳
1回答
为了尝试学习Idris，我决定尝试使用它来实现红黑树。经过一番努力，我设法让树本身通过了类型检查器，现在我正在尝试定义一个insert函数，顾名思义，它将一个元素插入到红黑树中。在其当前的，相当不完整的状态下，我的代码的相关部分如下所示： data Color : Type where
Red : Color
Black : Color
mutual
data RedBlackTree : (Ord key_type) => Nat -> Color -> (key_type : Type) -> Type -> Type where
浏览 18提问于2021-03-28得票数 3
我正在尝试在Idris中尽可能多地实现System F(多态λ演算)。我现在面临一个问题，我想用一个例子来演示：
data Foo = Bar Nat
Eq Foo where
(Bar _) == (Bar _) = True
data Baz: Foo -> Type where
Quux: (n: Nat) -> Baz (Bar n)
Eq (Baz f) where
(Quux a) == (Quux b) = ?todo
如您所见，任何两个Foo值都是相等的。我现在希望能够在定义Baz f上的等式时使用这一事实：Quux a具有类型Baz (Foo a)，Q
浏览 2提问于2016-09-17得票数 3
我正在尝试设置Azure Pipeline来为各种平台生成Idris1二进制文件： from head，并使用它为各种平台构建Idris2Head：。
我一直在尝试遵循这里的文档：
我想不出如何获得使其在Idris 2上工作所需的确切YAML。
Idris 1管道在这里：
Idris 2管道在这里：
# Test on Linux
- job: Linux
pool:
vmImage: 'ubuntu-16.04'
steps:
- script: |
echo Collection ID is $(System
浏览 2提问于2019-07-22得票数 2
1回答
定义 ZZ : Type
ZZ = (Nat, Nat) 然后是下面的代码 ZZ_greater_than_zero : ZZ -> Bool
ZZ_greater_than_zero (Z, Z) = False
ZZ_greater_than_zero (Z, (S n)) = False
ZZ_greater_than_zero ((S m), Z) = True
ZZ_greater_than_zero ((S m), (S n)) = ZZ_greater_than_zero (m, n) 给了我 10 | ZZ_greater_than_zero (Z, Z) = Fals
浏览 16提问于2020-03-26得票数 1
1回答
对于C函数，我调用的函数返回一个int，表示gt、eq或lt。我想撞上除了1，0或-1以外的任何东西，因为那是不应该发生的。我希望Idris认为0，1和-1是完全匹配的。我试过了
prim__compare : Scalar -> Scalar -> Int
Ord Scalar where
compare x y = case prim__compare x y of
-1 => LT
0 => EQ
1 => GT
浏览 3提问于2021-11-27得票数 0
回答已采纳
在文件中，它说：
Idris中的平等是异构的，这意味着我们甚至可以在不同类型的值之间提出平等：
idris_not_php :2= "2“
这个特殊的例子可以编译，但是这个洞是fromInteger 2 = "2"类型的。考虑到fromInteger 2可以属于Num实例的任何类型，那么编译器可能不够聪明，无法推断2的值不是String。
相比之下，以下略有不同的代码无法编译：
idris_not_php : S (S Z) = "2"
编译器报告Nat和String之间的类型不匹配。
此外，以下内容也成功编译：
Num String where
浏览 2提问于2017-07-21得票数 1
idris中有一个函数计数，定义为：
count : Eq a => a -> Vect n a -> Nat
count x [] = Z
count x (y::ys) = with (x == y)
| True = S (count x ys)
| False = count x ys
并且可以返回最大值计数的证明：
countLTELen : Eq a => (x : a) -> (l : Vect n a) -> LTE (count x l) n
countLTELen x [] = lteRefl
countLteLen x (y::
浏览 1提问于2018-06-16得票数 0
回答已采纳
1回答
在以下代码中
Idris> :t \x => x + x
\x => x + x : Integer -> Integer
Idris为x变量派生了一个Integer类型，我认为它应该得到一个接口限制，如Haskell中的那样：
Haskell> :t (\x y -> x + y)
(\x y -> x + y) :: Num a => a -> a -> a
然后，它甚至不像一个整数，接受双重类型：
Idris> (\x => x + x) 2.0
4.0 : Double
有人能给我解释一下吗？
浏览 2提问于2017-08-13得票数 1
回答已采纳
为什么Idris要求函数按照其定义和用mutual声明的相互递归的顺序显示
我希望Idris执行函数之间的第一次依赖分析，并自动重新排序。我一直相信Haskell会这么做。为什么在伊德里斯不可能这样做？
浏览 3提问于2014-11-01得票数 14
回答已采纳
Coq是一个证明助手，而Agda/Idris是编程语言(尽管它们可以被称为证明助手)。
我正在探索这些语言，我想知道Agda/Idris是否足以做Coq所能做的一切。
那么，有没有一些证据/管理代码/IDE (Emacs)函数的方法/其他Coq可以做而Agda/Idris不能做的事情呢？
浏览 21提问于2017-12-16得票数 9
回答已采纳
3回答
Agda和Idris都有效地禁止了Type类型值的模式匹配。看起来Agda总是在第一种情况下匹配，而Idris只是抛出一个错误。
那么，为什么打字是件坏事？它会破坏一致性吗？我还没有找到很多关于这个话题的信息。
浏览 8提问于2014-04-22得票数 50
回答已采纳
为什么下面的类型检查不会：
v1 : mod 3 2 = 1
v1 = Refl
然而，这将很好地检查类型：
v2 : 3 - 2 = 1
v2 = Refl
浏览 3提问于2017-06-21得票数 4
回答已采纳
我目前正在学习模型检查(模态逻辑、LTL、CTL、SAL模型检查等)。在业余时间，我正在学习Idris，这是一种支持依赖类型的强类型函数式编程语言。由于我同时查看模型检查和Idris，我开始对Idris与正式方法和模型检查的关系感到好奇。
当学习模型检查时，感觉所提到的大多数示例要么是关于验证以命令式方式编写的系统，要么是关于硬件组件。因此，我对强类型函数式编程语言中的模型检查的相关性感到困惑，特别是在Idris这样的依赖类型语言中，在我看来，类型检查器在验证正确性方面已经做得非常出色。然而，我的直觉告诉我，模型检查可能与不给出任何终止承诺的部分函数相关。
当使用强依赖的类型化编程语言(如Id
浏览 4提问于2016-04-07得票数 10
回答已采纳
1回答
根据
Idris类型检查器知道Lazy类型，必要时在Lazy a和a之间插入转换，反之亦然。
例如，b1 && b2被转换为b1 && Delay b2。Idris在决定将这些隐式转换放在哪里时使用哪些特定规则？
浏览 1提问于2021-11-16得票数 4
回答已采纳
2回答
我开始深入研究依赖类型编程，并发现Agda和Idris语言最接近Haskell，所以我从那里开始。
我的问题是:它们之间的主要区别是什么？类型系统在这两种语言中的表现形式是否相同？如果能有一个全面的比较和关于好处的讨论，那就太好了。
我已经发现了一些：
Idris有类似于Haskell的类型类，而Agda使用实例argumentsIdris包括一元和应用符号，它们似乎都有某种可重新绑定的语法，尽管不能真正确定它们是否相同。
编辑:这个问题的Reddit页面上有更多的答案：
浏览 75提问于2012-02-28得票数 181
回答已采纳
Type 1的居民既不是Type也不是Type的居民的示例是什么？当我在Idris REPL中探索的时候，我想不出任何东西。
更准确地说，我正在寻找Type之外的一些x，它会产生以下结果：
Idris> :t x
x : Type 1
浏览 0提问于2014-11-12得票数 5
我正在编写一个函数来测试Nat的命题相等性，它在IDRIS1中进行了类型检查。 sameNat : (n : Nat) -> (m : Nat) -> Maybe (n = m)
sameNat Z Z = Just Refl
sameNat (S n) (S m) = case sameNat n m of
Just e => Just (cong e)
Nothing => Nothing
sameNat _ _ = Nothing 但在Idris 2 (0.4.0)中
浏览 33提问于2021-09-19得票数 2
回答已采纳
1回答
如何在Idris REPL中编写函数？如果我在REPL中输入函数定义longer: string -> string -> string，我会得到以下错误信息：
(input):1:7: error: expected: "$",
"&&", "*", "*>", "+", "++", "-",
"->", ".", "/", "/=", "::",
浏览 1提问于2017-07-12得票数 7
回答已采纳
在Idris中，可以在函数类型声明中显式命名参数，如
length : (str : String) -> Nat
但是，当我试图命名返回值时，如
length : (str : String) -> (lengthOfStr : Nat)
idris编译器抛出一个错误。
期望"->“的输入意外结束
为什么命名参数的语法不适用于返回值？是否有一种方法可以在Idris中命名返回值(这样可以在doc-string中引用它们)？
浏览 0提问于2018-01-19得票数 2
回答已采纳
1回答
直到我遇到，我才意识到Idris有一个准引号。
以下是REPL中的一个简短示例：
Idris> :module Language.Reflection
Idris> `(S Z)
App (P (DCon 1 1)
(NS (UN "S") ["Nat", "Prelude"])
(Bind (MN 0 "_t")
(Pi (P (TCon 0 0) (NS (UN "Nat") ["Nat", "Prelude"])
浏览 2提问于2016-08-27得票数 2
回答已采纳
因此，在Idris中，编写以下内容是完全有效的。
item : (b : Bool) -> if b then Nat else List Nat
item True = 42
item False = [1,2,3] // cf. https://www.youtube.com/watch?v=AWeT_G04a0A
如果没有类型签名，这看起来就像动态类型化语言。但是，确实，伊德里斯是可靠的类型。item b的具体类型只能在运行时确定.
当然，这是一个Haskell程序员的谈话: Idris意义上的item b类型是在编译时给出的，它是if b then Nat ...。
现在我的问
浏览 4提问于2016-05-21得票数 33
回答已采纳
我试图定义一个名为byteWidth的函数，它捕获了“获取特定原子类型的字节宽度”的用法。
我的第一次审判：
byteWidth : Type -> Int
byteWidth Int = 8
byteWidth Char = 1
Idris编译器抱怨道：“当检查byteWidth的左手侧时:在左侧没有显式类型: Int”。
我的第二次审判：
interface BW a where
byteWidth : a -> Int
implementation BW Int where
byteWidth _ = 8
implementation BW Char wher
浏览 3提问于2018-02-02得票数 10
回答已采纳
2回答
我想写一个函数，它接受两个自然参数，并返回它们相等的证明。
我在试着
equal : (a: Nat) -> (b: Nat) -> Maybe ((a == b) = True)
equal a b = case (a == b) of
True => Just Refl
False => Nothing
但是我得到了以下错误
When checking argument x to constructor Prelude.Maybe.Just:
Type mismatch between
True = T
浏览 2提问于2017-10-20得票数 5
回答已采纳
当我试图将一个整数除以另一个整数时，我会得到以下消息：
Idris> 6 / 8
Can't find implementation for Fractional Integer
这到底是什么意思？，我如何在Idris中使用有理数？
浏览 2提问于2017-07-23得票数 2
回答已采纳
我试图使用Idris接口实现一个简单的代数结构层次结构。守则如下：
module AlgebraicStructures
-- definition of some algebraic structures in terms of type classes
%access public export
Associative : {a : Type} -> (a -> a -> a) -> Type
Associative {a} op = (x : a) ->
(y : a) ->
浏览 3提问于2016-06-11得票数 8
回答已采纳
我预期这个值为3，但得到了一个错误：
Idris> :let x = Just 2
Idris> 1 + !x
(input):1:3-4:When checking an application of function Prelude.Interfaces.+:
Type mismatch between
Integer (Type of (_bindApp0))
and
Maybe b (Expected type)
我也试过这个，没有一个托普莱尔绑定，并得到
Idris> l
浏览 3提问于2017-03-23得票数 3
回答已采纳
1回答
在Idris中，您可以在Fin n和(x ** So (x < n))之间建立同构吗？(我实际上并不了解Idris，因此这些类型可能无效。一般的想法是，我们有一个通过构造保证小于n的数据类型，另一个通过测试保证小于n的数据类型。)
浏览 3提问于2016-03-22得票数 0
给定来自的以下内容
import Data.Vect
data EqNat : (num1 : Nat) -> (num2 : Nat) -> Type where
Same : (num : Nat) -> EqNat num num
sameS : (eq : EqNat k j) -> EqNat (S k) (S j)
sameS (Same n) = Same (S n)
checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (E
浏览 0提问于2017-02-27得票数 1
1回答
Idris热切评价
、、、、
在Haskell中，我可以这样实现if：
if' True x y = x
if' False x y = y
spin 0 = ()
spin n = spin (n - 1)
这符合我的预期
haskell> if' True (spin 1000000) () -- takes a moment
haskell> if' False (spin 1000000) () -- immediate
在Racket中，我可以实现这样一个有缺陷的if：
(define (if2 cond x y) (if cond x y))
(define
浏览 2提问于2014-04-18得票数 31
回答已采纳
我有个玩具
对于UI，我使用编译为C的Vala代码，以便在UI中显示来自Idris的消息。
在Idris和Vala/C端，我都有一个方法来设置指向Idris函数的指针。因此，在Vala代码中可以看到：
global::afni = fn;
它使用指向函数Idris的指针设置一个全局变量。稍后，在另一个Vala方法中，我调用：
int res = global::afni(0);
string da_label = @"blah $res";
Gtk.Label label = new Gtk.Label (da_label);
因此，我调用comFn函数
浏览 3提问于2019-09-05得票数 2
回答已采纳
如何在Idris 1.3.3中生成随机整数？
不起作用的示例程序：
module Random
import Effect.Random --This gets me access to the rndInt function
我按如下方式运行该程序：
idris random.idr -p effects
尝试在REPL中使用rndInt函数，我得到以下错误消息：
*random> rndInt 1 10
(input):Can't infer argument m to rndInt
请在您的答案中包含完整的源代码。谢谢。
浏览 1提问于2021-05-23得票数 0
目前，我在使用随nixpkg一起安装的Idris包时遇到了一些问题，该包位于依赖它的另一个Idris包中。这两个包都已经在Debian系统上进行了测试，所以问题不在于Idris代码本身，而在于它们在NixOS系统上的安装方式。我相信我可以通过调用nix-env -f math.nix -i idris_math成功安装第一个包，其中math.nix的定义如下：
with import <nixpkgs> { };
stdenv.mkDerivation rec {
name = "idris_math";
idris = haskellPackages.i
浏览 0提问于2017-03-18得票数 3
在第6章的代码中，我对以下代码感到困惑：
data DataStore : Type -> Type where
MkData : (size : Nat) ->
(items : Vect size schema) ->
DataStore schema
我认为它可能无法编译，因为schema似乎是未定义的，或者至少需要以某种方式绑定到DataStore的第一个参数。但是，它加载得很好，可以像这样使用：
*DataStore> the (DataStore String) $ MkData 2 ["F
浏览 3提问于2016-08-27得票数 4
回答已采纳
My集合返回包含以下字段的集合：
<d:ColorFlagInfo>Red,Blue</d:ColorFlagInfo>
<d:ColorFlagInfo>Red,Green</d:ColorFlagInfo>
<d:ColorFlagInfo>Black,Brown</d:ColorFlagInfo>
请有人帮助我构建一个Odata查询，该查询通过一个或多个特定的颜色过滤：
我尝试了以下方法来获得特定的颜色：
？$filter=substringof(‘Black’，ColorFlagInfo)
?$filter=
浏览 4提问于2014-06-25得票数 0
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
即时通信 IM
实时音视频活动推荐
腾讯云开发者
