Mathlib4 Help¶
本页面是Seasawher mathlib4-help的翻译。它保存了 #help
指令的输出,你可以在此查询各种接口,指令以及tactic的用法。
因为Mathlib更新频繁,原项目使用了Github Action实时生成新版页面。但我们希望人工校对来保证质量(暂时没有高质量且免费的翻译API),因此暂时不跟随Mathlib更新本页面。因此本页面的结果不保证时效性,仅供参考。
本页面是Seasawher mathlib4-help的翻译。它保存了 #help
指令的输出,你可以在此查询各种接口,指令以及tactic的用法。
因为Mathlib更新频繁,原项目使用了Github Action实时生成新版页面。但我们希望人工校对来保证质量(暂时没有高质量且免费的翻译API),因此暂时不跟随Mathlib更新本页面。因此本页面的结果不保证时效性,仅供参考。