相关疑难解决方法(0)

我刚刚发现了最大和非最大参数的存在(参见https://coq.inria.fr/refman/Reference-Manual004.html#sec109).

但是有一些动机使用一个而不是另一个吗？一个比另一个更近？仅需要{}创建最大隐式参数,而必须使用Arguments或Implicit Arguments指定非最大参数.是否应该首选最大隐式参数？