Coq에서 암시 적 인수를 명시 적으로 어떻게 제공합니까?

Question

f : x -> y -> z이라는 정의가 있다고 가정하면 x을 쉽게 추론 할 수 있습니다. 을 사용하여 x에 암시 적 인수를 사용하도록 선택했습니다.

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

예를 들어 암시 적 인수를 이름으로 전달합니다. 이렇게하면 어떤 인수가 전달되는지 명확히 알 수 있으며 다른 인수에 _을 전달하지 않고도 일부 implicits를 전달할 수 있습니다.

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. 

결과 :

Check @id nat 1. 

또한 (a:=v)을 사용할 수 있습니다 : 모든 implicits를 제거하고 명시 적으로 제공하기 위해 @로 이름을 붙일 수

id 1 
    : nat