Menu
Suppose I have a definition f : x -> y -> z where x can be easily inferred.
I therefore choose to make x an 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).
Clearly S = nat can be and is inferred by Coq, and Coq replies:
id 1
: nat
However, at a later time, I want to make the implicit 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 possible at all? If so, what is the appropriate syntax?
318
Implicit arguments are arguments that occur in Logical Form, but are omitted in the syntax. Consider the following sentences: (1) Mary was run over by a car. (2) Mary was run over with a car.
Implicit and dynamic parameters are proposed as a general means to reduce the length of argument lists of function calls without resorting to dangerous global variables. In C++, these new kinds of parameters constitute a generalization of parameters with default arguments, whose values can be omitted in function calls.
The implicit parameter in Java is the object that the method belongs to. It's passed by specifying the reference or variable of the object before the name of the method. An implicit parameter is opposite to an explicit parameter, which is passed when specifying the parameter in the parenthesis of a method call.
You can prepend the name with @ to remove all implicits and provide them explicitly:
Check @id nat 1.
You can also use (a:=v) to pass an implicit argument by name. This can both clarify what argument is being passed and also allows you to pass some implicits without passing _ for the others:
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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
