The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

Definition fst_comp `(Comparable A) (a b:A):A :=š if compare a b then
a else b.About fst_comp.
(*fst_comp : forall A : Type, Comparable A -> A -> A -> A

Argument A is implicit and maximally inserted
Argument scopes are [type_scope _ _ _]
fst_comp is transparent
Expands to: Constant Top.fst_comp*)

Definition fst_comp2 `{Comparable A} (a b:A):A :=
  if compare a b then a else b.
About fst_comp2.

(*fst_comp2 : forall A : Type, Comparable A -> A -> A -> A

Arguments A, H are implicit and maximally inserted
Argument scopes are [type_scope _ _ _]
fst_comp2 is transparent
Expands to: Constant Top.fst_comp2
*)

H is also maximally inserted.

2011/11/4 Victor Porton 
<porton AT narod.ru>:
> 04.11.2011, 21:57, "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 *)
>
> But what is the difference of `(...) and `{...}.
>
> The Reference Manual is silent on this question :-(
>
> --
> Victor Porton - http://portonvictor.org
>