是什么让自然数在超时方面如此特别？

作者: 冷月如霜·胡狼
发布时间: 2024-11-08 12:17:04 (2天前)
转自：

2 条回复

0#
回复此人
满目山河 | 2019-08-31 10-32

<div class =“post-text”itemprop =“text”> <P> <code> real </code> 是一个定义，所以它也会减少： </p> <pre> <code> def real := @cau_seq.completion.Cauchy ? _ _ _ abs _ </code> </pre> <P> <a href="https://github.com/leanprover/mathlib/blob/a243126efbd7ddef878876bb5a1bb3af89f2e33b/data/real/basic.lean#L12" rel="nofollow noreferrer"> https://github.com/leanprover/mathlib/blob/a243126efbd7ddef878876bb5a1bb3af89f2e33b/data/real/basic.lean#L12 </A> </p> <P> 实际上，这是一个复杂的（没有双关语）定义，可能取决于数十个或数百个其他定义。递归地减少所有这些将花费很长时间并创建一些巨大且完全无益的输出。 </p> <P> 另一方面， <code> nat </code> 是一种无参数的电感类型。没有什么可以减少的。 </p> </DIV>

编辑

登录后才能参与评论