仓库源文，站点原文

此答被折叠后，就着手试用litex。在线环境 运行：

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
小怪 $友好 小怪

效果如下，输出比较繁杂：

希望项目早日整理可批量自动运行的测试用例集，以提高可靠性和可维护性，进而提高新人加入合作动力。木兰语言重现项目的 首次合作任务 以通过包括已有用例在内的测试为目标之一，供参考。

更希望早日完成中英对照术语表，比如 这样，并将反馈信息与语法中 相关元素一致化。

貌似暂不支持解方程，接下去根据自己需要先用z3解一次方程。