The Coq mailing list

[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) *****

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!