代码8.5pl1中的精炼和@(At)符号 [英] Refine and @ (at) symbol in Coq 8.5pl1

问题描述

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

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

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

推荐答案

您正在寻找simple refine。

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

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

这篇关于代码8.5pl1中的精炼和@(At)符号的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！