coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Victor Porton <porton AT narod.ru>
To: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
Cc: Thomas Braibant <thomas.braibant AT gmail.com>, coq-club AT inria.fr
Subject: Re: [Coq-Club] Why backtick notation is needed?
Date: Fri, 04 Nov 2011 22:33:55 +0400
Envelope-from: porton AT yandex.ru

Compiling this:

<<<
Definition X `{T: Type} (A: T) := O.
Definition Y {T: Type} (A: T) := O.

Print X. Print Y.
>>>

tells that both X and Y have an implicit and maximally inserted argument.

I don't understand what is the difference of `{...} and {...}.

Please explain and also please tell this in Reference Manual clearly.

--
Victor Porton - http://portonvictor.org

[Coq-Club] Why backtick notation is needed?, Victor Porton
- Re: [Coq-Club] Why backtick notation is needed?, Thomas Braibant
  - Re: [Coq-Club] Why backtick notation is needed?, Victor Porton
    - Re: [Coq-Club] Why backtick notation is needed?, Alexandre Pilkiewicz
  - Re: [Coq-Club] Why backtick notation is needed?, Alexandre Pilkiewicz
    - Re: [Coq-Club] Why backtick notation is needed?, Victor Porton
      - Re: [Coq-Club] Why backtick notation is needed?, Alexandre Pilkiewicz