The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

The back-tick is related to type-classes, not to implicit arguments.
In your example, you do not deal with implicit arguments. Check the
following exceprt: there, id2 has an implicit argument, while id1 does
not have one (which requires to give this argument by hand, while it
can be inferred from the context).

Definition id (A : Type) (x : A) := A.šDefinition id2 {A : Type} (x : A) := A.
Check id2 1.šCheck id 1.š(* fails *)
Check id nat 1. (* succeeds *)

thomas



On Fri, Nov 4, 2011 at 6:48 PM, Victor Porton 
<porton AT narod.ru>
 wrote:
> I installed Coq 8.3.
>
> The following:
>
> <<<
> Definition id `(x : nat) : nat := x.
> Print id.
>
> Definition id2 (x : nat) : nat := x.
> Print id2.
>
> Definition v := id O.
> Definition v2 := id2 O.
>
> Print v.
> Print v2.
>>>>
>
> Produces the output:
>
> <<<
> id = fun x : nat => x
> š š : nat -> nat
>
> Argument scope is [nat_scope]
> id2 = fun x : nat => x
> š š : nat -> nat
>
> Argument scope is [nat_scope]
> v = id 0
> š š : nat
> v2 = id2 0
> š š : nat
>>>>
>
> You see that types of id and id2 are identical.
>
> Moreover not only id but also id2 works with an implicit argument.
>
> What is the point to use backtick, if it work implicitly even without it?
>
> --
> Victor Porton - http://portonvictor.org
>