linear_solver:设计为易于与Rust枚举一起使用的线性求解器

linear_solver 设计为易于与Rust枚举一起使用的线性求解器。 这是一个用于自动定理证明的库。 线性求解意味着可以用其他事实代替某些事实。 该技术还可用于使定理证明更加有效。 如果您正在寻找无法删除事实的求解器， 参见 注意！ 此求解器不支持多个历史记录。 它假设事实被简化后，它们证明了相同的事实集而没有简化。 线性求解器可用于： 证明线性逻辑中的一些东西 更有效率地证明经典逻辑中的某些事物 证明一些有关“消耗”资源的地方 约束解决 实现一些约束解决程序设计语言 该项目受到极大启发 示例：步行 /* In this example, we reduce a walk (left, right, up, down): l, l, u, l, r, d, d, r ---------------------- l, u */ extern cr