Update README

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

.github/README.md

@@ -1,7 +1,61 @@
 # lyzh
 
+```rs
+fn f(t: type) -> type { t }
+```
+
 一款用于教学目的的依赖类型语言, 献给 [Lyzh].
 
+需要使用 Python 3.12 版本. 执行以下命令运行一个文件:
+
+```bash
+python -m lyzh example.lyzh
+```
+
+整个代码仓库的代码量:
+
+* 不包括注释: 650 行左右
+* 不包括注释和文本解析部分: 420 行左右
+
+由于整个类型系统里面能用的东西不多, 所以很难写一些真正有意义的事情, 所以这里建议大家把代码用自己喜欢的语言抄一遍,
+然后阅读自己喜欢的纸, 往自己的语言里面添加 `string`, `number`, `i32`, tuple, enum, record, 这样那样好玩的类型吧!
+
+当然了, 一些 function pearls 还是可以玩的. :)
+
+比如说 Church numerals:
+
+```rs
+fn nat -> type {
+    (t : type) -> (s: (n: t) -> t) -> (z: t) -> t
+}
+
+fn add(a: nat) (b: nat) -> nat {
+    |t| { |s| { |z| { ((a t) s) (((b t) s) z) } } }
+}
+
+fn mul(a: nat) (b: nat) -> nat {
+    |t| { |s| { |z| { ((a t) ((b t) s)) z } } }
+}
+```
+
+比如说 Leibniz equality:
+
+```rs
+fn eq(t: type) (a: t) (b: t) -> type {
+    (p: (v: t) -> type) -> (pa: p a) -> p b
+}
+
+fn refl(t: type) (a: t) -> ((eq t) a) a {
+    |p| { |pa| { pa } }
+}
+
+fn sym(t: type) (a: t) (b: t) (p: ((eq t) a) b) -> ((eq t) b) a {
+    (p (|b| { ((eq t) b) a })) ((refl t) a)
+}
+```
+
+用这几个定义来写点好玩的小证明吧!
+
 [Lyzh]: https://github.com/imlyzh
 
 ## License

lyzh/concrete/elab.py

@@ -130,21 +130,27 @@ def infer(self, e: cst.Expr) -> typing.Tuple[ast.Term, ast.Term]:
         raise AssertionError("impossible")
 
     def guarded_check(
-        self, p: core.Param[ast.Term], e: cst.Expr, typ: ast.Term
+            self, p: core.Param[ast.Term], e: cst.Expr, typ: ast.Term
     ) -> ast.Term:
         """在 p 的保护下 (即将 p 加入到本地变量中, 检查完毕后删除), 检查表达式 e 的类型是否为 typ."""
         self.locals[p.name.id] = p.type
         ret = self.check(e, typ)
-        del self.locals[p.name.id]
+        try:
+            del self.locals[p.name.id]
+        except KeyError:
+            pass
         return ret
 
     def guarded_infer(
-        self, p: core.Param[ast.Term], e: cst.Expr
+            self, p: core.Param[ast.Term], e: cst.Expr
     ) -> typing.Tuple[ast.Term, ast.Term]:
         """在 p 的保护下 (即将 p 加入到本地变量中, 推导完毕后删除), 推导表达式 e 的类型."""
         self.locals[p.name.id] = p.type
         ret = self.infer(e)
-        del self.locals[p.name.id]
+        try:
+            del self.locals[p.name.id]
+        except KeyError:
+            pass
         return ret
 
     def nf(self) -> normalize.Normalizer: