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*)
は、すべての可能なこのですか? もしそうなら、適切な構文は何ですか?