了解Coq中的复合类型[软件基础]
Software Foundations, Basics, Compound Types
我试图理解Coq (第二天，请耐心听我说，如果这很愚蠢的话，我很抱歉)，但我正在阅读软件基础一书中关于复合类型的部分，并试图理解这一点：
Inductive rgb : Type :=
| red : rgb
| green : rgb
| blue : rgb.
Inductive color : Type :=
| black : color
| white : color
| primary : rgb → color.好的，这些都是协归纳类型，我的问题是“主要”的定义。我看到rgb是一个枚举类型，部分颜色是枚举类型，但是primary是一个函数。
问题是，它看起来像是一个接受rgb并返回颜色的函数，然而该部分(单色，isred)中的所有示例都返回布尔值。
它看起来也像是我们在书中一直使用的反射性属性(同样，就像第1页，听我说)，看起来它采用了您的策略，并证明了等价性；到目前为止，我们所有的示例都是boolean = boolean格式的。
我们需要一个函数的定义，该函数接受rgb，并返回颜色，我们可以使用反射率(因为这是我们在第1页上所知道的全部)来求解，对吧？用于单元测试？
我在正确的轨道上吗？我想我只是被单色和isred的引入搞糊涂了，它们又回到了使用布尔值的时候，这似乎不是我们试图解决的问题，以获得有效的颜色示例。
回答 1
Stack Overflow用户
发布于 2018-08-15 05:16:29
(首先：
这些都是共归纳类型
这些实际上是归纳类型，但这可能是一个打字错误。)
它看起来像是一个接受rgb的函数，并返回一种颜色
是的，这就是primary：一个接受rgb元素并返回color元素的函数。这是一种特殊类型的函数，称为构造函数。构造函数与正则函数的不同之处在于，归纳类型的每个元素都是从该类型的一个构造函数获得的。在第一章中，还有由模式匹配定义其他函数，例如monochrome。该函数返回一个布尔值，但我们也可以有其他返回color的函数。例如：
Definition flip_color (c : color) : color :=
match c with
| white => black
| black => white
| primary _ => c
end. 自反性属性...采用你的策略，并证明平等
关于术语的说明:在这种情况下，reflexivity是一种策略，并不将任何策略作为参数。然而，你是对的，它是用来证明等式的。
我们需要一个函数的定义，这个函数接受rgb，并返回颜色，我们可以使用反射率(因为这是我们在第1页上所知道的全部)来求解，对吧？
？用于单元测试？
你说的是什么单元测试？本章提到了orb和binary类型的单元测试，但没有针对color的测试。
https://stackoverflow.com/questions/51849223
复制相似问题