由网友(上课ゾ打瞌睡)分享简介：在以前的Coq版本中，使用符号@in Reine命令允许我创建一个循序渐进的证明。(每个参数都是单独的目标。)我希望避免像"？goal0？goal1"这样的隐式参数。现在我做不到了。我应该怎么做才能获得这种可能性？(这对我来说非常不舒服，尤其是当我尝试处理递归函数时。)推荐答案您正在寻找simple refine。...

在以前的Coq版本中，使用符号@in Reine命令允许我创建一个循序渐进的证明。(每个参数都是单独的目标。)

我希望避免像"？goal0？goal1"这样的隐式参数。现在我做不到了。 我应该怎么做才能获得这种可能性？

(这对我来说非常不舒服，尤其是当我尝试处理递归函数时。)

推荐答案

您正在寻找simple refine。

在8.5中，可以通过统一(所谓的隐式)解决的目标被放在"搁置"的隐藏区域中，因为它们被认为是微不足道的。您可以使用Unshelve取消搁置它们，但这有点不方便，因为它是本土化的命令。

simple refine表现为8.4，不会将任何内容放在货架上。