coq - 如何在 Coq 中显式提供隐式参数？

Question

假设我有一个定义 f : x -> y -> z哪里x可以很容易地推断出来。
因此我选择制作 x使用 Arguments 的隐式参数.

考虑以下示例:

Definition id : forall (S : Set), S -> S :=
fun S s => s.

Arguments id {_} s.

Check (id 1).

清楚 S = nat可以并且被 Coq 推断，Coq 回复:

id 1
     : nat

但是，稍后，我想使隐式参数显式，例如，为了可读性。

换句话说，我想要类似的东西:

Definition foo :=
 id {nat} 1. (* We want to make it clear that the 2nd argument is nat*)

这可能吗？
如果是这样，适当的语法是什么？

Answer 1

您可以在名称前加上 @删除所有隐式并明确提供它们:

Check @id nat 1.

您也可以使用 (a:=v)按名称传递隐式参数。这既可以澄清正在传递的参数，也可以让您传递一些隐式而不传递 _对于其他人:

Check id (S:=nat) 1.

Definition third {A B C:Type} (a:A) (b:B) (c:C) := c.
Check third (B:=nat) (A:=unit) tt 1 2.