@GeruzoniAnsasu #8

> 列举的所有 !check <exp>:<type>我都没看到结论，即断言为真还是假，搞得我一头雾水

这个 check! 的意思是要求编译器进行类型检查，即 check <exp> against <type>，如果 <exp> 确实是 <type> 的 inhabitant （或者说 <exp> 具有 <type> 类型），则检查通过。否则应该产生一个类型错误。

> 本来还以为有什么可等性的定义方法，或者可等类型是什么特殊类型。然而似乎也不是。是说 Equal 这个三元组是一个抽象类型？我就搞不懂了如果「 Equal(X,Y,Z)三元组」

「相等类型」相关的内容非常复杂，与这门语言选择的类型论有关。我太菜了，可能回答不了这个问题。

> 那这样理解的话 Equal()也是一个泛型，List 的参数列表是类型，Equal 里却可以有表达式……为什么？规范是啥……

这是 dependent type （依值类型），即类型可以依赖值。在 DT 的语言中，类型和值并没有什么不同。

> ctrl+f 了一下没看到 return induction ( 这个 induction 函数是哪讲的就放弃了

这个 induction 可以视为「模式匹配」，是编译器内建的操作（比如 rust 的 match ），是一种对归纳数据类型（比如 Nat 类型）归纳证明的一种方法。你可以理解为「分类讨论」。

> 文档全文也没看出来如何 prove something ，甚至如何定义公理都没讲明白

文档这一部分： https://readonly.link/manuals/gitlab.com/cicada-lang/cicada/-/datatype/01.1-proving-theorems-about-nat.md
以加法交换律为例展示了证明，即：add_commute(x: Nat, y: Nat,): Equal(Nat, add(x, y), add(y, x))
这个函数签名的意思是：对于任意两个自然数 x y ，都有 x + y = y + x
而这个函数的 body 就是对这个命题的证明。
关于这个问题，更多可以参考： https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence