Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Why backtick notation is needed?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Why backtick notation is needed?


chronological Thread 
  • From: Victor Porton <porton AT narod.ru>
  • To: Thomas Braibant <thomas.braibant AT gmail.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Why backtick notation is needed?
  • Date: Fri, 04 Nov 2011 22:06:21 +0400
  • Envelope-from: porton AT yandex.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



Archive powered by MhonArc 2.6.16.

Top of Page