2017-12-18 9 views
4

f : x -> y -> zという定義があるとします。ここで、xは簡単に推測できます。 を使用してxに暗黙の引き数を設定することを選択しました。Coqで暗黙の引数を明示的に指定するにはどうすればよいですか?

は、次の例を考えてみましょう:

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

Arguments id {_} s. 

Check (id 1). 

明らかにS = natが可能とコックによって推定され、そしてコックは返信:

id 1 
    : nat 

しかし、後の時点で、私は暗黙のを作りたいです引数は、例えば、読みやすくするために明示的に指定します。言い換えれば

、私のような何かをしたいと思います:

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

は、すべての可能なこのですか? もしそうなら、適切な構文は何ですか?

答えて

4

例えば 暗黙の引数を名前で渡す。これにより、どの引数が渡されているかを明確にすることができ、また、他の引数に対して_を渡さずにいくつかの暗黙的な引数を渡すことができます。

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. 
2

可能な方法の1つは、定義に@を追加することです。

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

Arguments id {_} s. 

Check @id nat 1. 

結果に:

Check @id nat 1. 

ます。また(a:=v)を使用することができます:あなたはすべての暗黙を削除し、それらを明示的に提供するために、@と名前を付加することができます

id 1 
    : nat 
関連する問題