Metamath-rs - 用于处理Metamath数据库的库

什么是一个什么？

Metamath是一种用于表达数学形式证明的语言。Metamath对底层逻辑的假设很少，足够简单，可以支持各种工具。参见 http://us.metamath.org/#faq。

Metamath-rs可以快速验证这些证明，大大增强了证明正确性的信心。我们所说的“快速”是指：超过28,000个证明可以在不到一秒内被证明。

Metamath-rs是metamath-knife项目的库组件，该项目还包含一个独立的命令行应用程序。

• 它支持所有 Metamath证明格式。特别是，Metamath-knife增加了对所有 Metamath证明格式的支持（未压缩、压缩、包或显式）。
• 我们采取了额外的措施来防止错误，例如，我们有一个CI管道（使用GitHub actions实现）。
• 我们移除了已弃用的结构，例如，已弃用的try!(...)已被易于阅读的"?"结构所替代。
• 我们积极努力消除编译器警告。这往往可以减少错误，使代码更易于阅读，并提高性能（例如，通过消除不必要的clone()调用）。

许可证

本软件受以下任一许可证的许可：

• Apache License, Version 2.0 (LICENSE-APACHE 或 https://apache.ac.cn/licenses/LICENSE-2.0)
• MIT许可证 (LICENSE-MIT 或 http://opensource.org/licenses/MIT)

其许可证的SPDX许可证表达式为"(MIT OR Apache-2.0)"。

请注意，这与smetamath-rs (SMM3)的许可证完全相同，这是故意的，因为我们希望smetamath-rs (SMM3)能够在他们愿意的情况下重新整合我们所做的一切。

贡献

除非您明确声明，否则根据Apache-2.0许可证定义的，您有意提交以包含在作品中的任何贡献，均应双许可如上所述，不附加任何额外条款或条件。