How to explicitly provide implicit arguments in Coq?

Question

Suppose I have a definition f : x -> y -> zwhere xit can be easily deduced. So I want to make xan implicit argument using Arguments.

Consider the following example:

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

Arguments id {_} s.

Check (id 1).

It is clear that S = natCoq can be deduced, and Coq answers:

id 1
     : nat

However, at a later time, I want to make an explicit argument explicit, say, for readability.

In other words, I would like something like:

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

Is this even possible? If so, what is the appropriate syntax?

Answer 1

You can add a name using @to remove all implications and provide them explicitly:

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.

Answer 2

@ . :

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

Arguments id {_} s.

Check @id nat 1.

:

id 1
     : nat