初学者，不能精益进口

作者: 一瓶泡沫
发布时间: 2025-03-09 09:52:19 (6小时前)
转自：

3 条回复

0#
回复此人
明天会更好 | 2019-08-31 10-32

<div class =“post-text”itemprop =“text”> <P> 我通过直接联系Avigad教授得到了解决方案。 </p> <P> 事实证明，该书不仅使用标准库，还使用精益数学组件库， <a href="https://github.com/leanprover/mathlib" rel="nofollow noreferrer"> mathlib </A> 。安装它对我有用。我现在可以做 <code> import data.set </code> 没有收到错误。 </p> </DIV>

编辑
1#
回复此人
你瞎啊！撞我心了 | 2019-08-31 10-32

<div class =“post-text”itemprop =“text”> <P> 这些包隐藏在 <code> init </code> 。 </p> <pre> <code> import init.classical import init.data.nat import init.data.set </code> </pre> <P> 但我相信精益可以进口所有东西 <code> init </code> 默认情况下，您实际上不需要上面的行。 </p> <P> 你也可以跳过 <code> open </code> 并限定调用。 </p> <pre> <code> example (P : Prop) : P �� ? P := classical.em P </code> </pre> </DIV>

编辑

登录后才能参与评论