The Coq mailing list

[Victor Porton <porton AT narod.ru>]

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