值会 给出一个答案及其类型。例如： *prims> 6*6+6 42 : Integer *prims> x == 6*6+6 True : Bool 奉 奤 奲 奩 女 为原语类型定义了所有的普通算术和比较运算。它们通过接口进行了重载， 并可被扩展以适用于 用户定义的类型，这点我们会在 接口 夨 姩 妡妵 夲失天 一节中讨论。布尔表达式可通过 if...then...else 构 造来测试，例如： ot y p i n g） ） ） 时，它可在所有的证明细节结束前测试程序。 • 在 阅 阅 阅读 读 读 程序时，推迟证明的细节通常会让过程更清晰，避免读者从底层算法中分心。 临时定义的写法和普通定义相同，只是它以 ?= 而非 = 引入右式。我们将 parity 定义为： parity : (n:Nat) -> Parity n parity Z = Even {n=Z} parity (S 之外的世界建立「联系」。 例如，给定一个表示数据库模式（奓 奣 奨 奥 奭 奡）的类型， 和一个针对它检查过的查询，类型提供器可以在 进行类型检查时读取真实数据库的模式。 奉 奤 奲 奩 女 类型提供器使用普通的 奉 奤 奲 奩 女 可执行语义来运行 奉 奏 活动并提取出结果。 该结果会作为编译代码时 的常量被保存。它可以是个类型，此时它能像其它类型一样使用； 它也可以是个值，此时它也可以像 其它值一样使用，并作为一个索引被包含在类型中。