如何在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.