litex试用小结

Author: nobodxbodon

_posts/2026-01-23-浅尝litex证明编程语言.md

@@ -0,0 +1,37 @@
+
+[此答被折叠](https://www.zhihu.com/question/1965786839827854197/answer/1973021573339428510)后，就着手试用litex。[在线环境](https://litexlang.com/playground) 运行：
+
+```
+let 快乐宝贝 set
+let 小怪, 大怪, 老怪, 快乐超人 快乐宝贝
+
+# 传递性
+prop 领导(x, y 快乐宝贝)
+know 大怪 $领导 小怪, 老怪 $领导 大怪
+prop 层层领导(x, y, z 快乐宝贝):
+    x $领导 y
+    y $领导 z
+    <=>:
+        x $领导 z
+know forall x, y, z 快乐宝贝: x $领导 y, y $领导 z => $层层领导(x, y, z)
+$层层领导(老怪, 大怪, 小怪)
+老怪 $领导 小怪
+
+# 可交换性
+prop 敌对(x, y 快乐宝贝)
+know forall x, y 快乐宝贝 => x $敌对 y <=> y $敌对 x; 快乐超人 $敌对 大怪
+大怪 $敌对 快乐超人
+
+# 自反性
+prop 友好(x, y 快乐宝贝)
+know forall x 快乐宝贝 => x $友好 x
+小怪 $友好 小怪
+```
+
+效果如下，输出比较繁杂：
+
+希望项目早日整理可批量自动运行的测试用例集，以提高可靠性和可维护性，进而提高新人加入合作动力。木兰语言重现项目的 [首次合作任务](https://gitee.com/MulanRevive/mulan-rework/issues/I3QHKV) 以通过包括已有用例在内的测试为目标之一，供参考。
+
+更希望早日完成中英对照术语表，比如 [这样](https://github.com/litexlang/litex-official-documents/issues/9)，并将反馈信息与语法中 [相关元素一致化](https://www.zhihu.com/question/632589892/answer/3310126506)。
+
+貌似暂不支持解方程，接下去根据自己需要先用z3解一次方程。