布雷迪说，在使用Idris进行类型驱动的开发中，
如果您能够提供一个空类型的值，那么您将能够产生一个 any 类型的值。换句话说，如果您有证据证明发生了不可能的值，则可以执行任何操作。前奏提供了一个函数
void，该函数表示以下内容：
void : Void -> a
我很难理解这意味着什么。您如何从Void产生 any 类型的值？那这意味着您什么都可以做？如果您可以参考void
虚空如何让您产生或做任何事情？
•
问答
iCMS 回答：虚空如何让您产生或做任何事情？
每种类型都有一套引入规则和消除规则。虚空有点特别。它本身没有引入规则。但是，其他类型附带了针对Void的额外介绍规则。例如，Nat的相等性对Void有一个引入规则：
n: Nat -> 0 = S(n) -> Void
（Idris从其自己的内部规则生成这些规则，以确定不同的术语无法进行模式匹配。）
消除规则让您走另一条路，例如：
Void -> n: Nat -> 0 = S(n)
实际上，它说所有不可能的事都是同样不可能的-如果您拥有一件不可能的事，那么您也可以拥有任何其他不可能的事。
更深层的问题是：如果我们没有消除规则，将会发生什么？我们会以不同类别的不可能事物结束，并以不同程度的非等效可能性结束吗？
我不知道那个问题的答案。
但是，如果您假设0 = 1，则很容易证明任何事物都等于其他事物（因为您可以证明repeat（1，f，x）= repeat（0，f，x），因此f（对于所有x和f都为x）= x，因此在f（a）= y的地方定义f，则x = y）。
因此，如果我们知道Void的所有引入规则均来自不等式，则像下面这样的更有限的消除规则将等同于更通用的规则：
Void -> 0 = 1