Answers in README

Signed-off-by: Anqur <[email protected]>

README.md

@@ -54,7 +54,55 @@ fn sym(t: type) (a: t) (b: t) (p: ((eq t) a) b) -> ((eq t) b) a {
 }
 ```
 
-用这几个定义来写点好玩的小证明吧!
+用这几个定义来写点好玩的小证明吧! 哦对了, 有人说要我上传下习题的答案 (
+
+* 用 `nat`、`add`、`mul` 写一些简单的计算:
+
+<details>
+<summary>答案</summary>
+
+```rs
+fn three -> nat {
+    |t| { |s| { |z| { s (s (s z)) } } }
+}
+
+fn six -> nat {
+    (add three) three
+}
+
+fn nine -> nat {
+    (mul three) three
+}
+```
+
+比如, 输出结果能看到 `six` 内部有 6 个 `f`, 说明计算成功.
+
+</details>
+
+* 用 `eq`、`refl`、`sym` 写一些简单的证明:
+
+<details>
+<summary>答案</summary>
+
+```rs
+fn a -> type {
+    type
+}
+
+fn b -> type {
+    type
+}
+
+fn lemma -> ((eq type) a) b {
+    (refl type) a
+}
+
+fn theorem(p: ((eq type) a) b) -> ((eq type) b) a {
+    (((sym type) a) b) lemma
+}
+```
+
+</details>
 
 [Lyzh]: https://github.com/imlyzh
 

lyzh/abstract/rename.py

@@ -1,7 +1,12 @@
 """数值内部引用刷新器, 这是因为, 我们使用了 capture-avoiding substitution 的技术,
 所有的定义检查完毕类型之后, 它就像一个 "模板" 存在于 global context 当中, 如果后续有其他定义引用,
 则我们应该把这个 "模板" 生成出来的数值内部的所有 ID 重新刷新, 不然的话, 引用会指向 "模板" 中去,
-造成严重错误 (比如程序陷入死循环)."""
+造成严重错误 (比如程序陷入死循环).
+
+举个死循环的例子, 假如我们不去做 rename, 则有这样一个函数:
+
+TODO
+"""
 
 import dataclasses
 import typing