The Coq mailing list

[t x <txrev319 AT gmail.com>]

You're right, I should have read the 2nd paragraph of that link.

Thanks for providing the concrete example.

On Thu, Oct 10, 2013 at 12:53 AM, Cedric Auger <sedrikov AT gmail.com> wrote:

2013/10/10 t x <txrev319 AT gmail.com>

At http://coq.inria.fr/refman/Reference-Manual003.html , we have:

term ::=
  | forall binders, term

  | fun binders => term
  | ...

  | let ident [binders] [: term] := term in term
  | ...

binders ::= binder ... binder

binder ::=

  | name

  | ( name ... name : term )

  | ( name [: term] := term) *****

In the doc, there is a link to section 1.2.6: http://coq.inria.fr/refman/Reference-Manual003.html#sec31
in the grammar definition. It seems you did not follow this link. I have never used it. I guess it is some syntactic sugar for things like:

"fun (A : Type) => let (B := list A) in fun (x : B -> B) => …"

could be abbreviated in:

 
"fun (A : Type) (B := list A) (x : B -> B) => …"

thus avoiding one 'let' and one 'fun'

Now, what I don't understand is when *** is ever used.

When I'm using it from "let", the [: term] := term provides the "definition."

When I'm using from "forall", at most I use (x: A) (y: B) ... but no need for ":="
Similarly, when using "binders", I also use (x: A) (y: B) ... but no need for ":="

Thus, my question: when is the "****" form of binder ever used?

Thanks!

--
.../Sedrikov\...