The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Hi, without looking into the details, yes, the (x := y) notation is to set (implicit) argument x to y.

On Wed, Aug 14, 2013 at 3:26 AM, t x <txrev319 AT gmail.com> wrote:

With apologies for spamming, the following ( https://gist.github.com/anonymous/4d7e55a5aabbf8e2f001 ) seems to imply it's a way to set the implicit "ls2" argument of the concat function.

If someone could confirm this understanding is correct, I'd appreciate it.

Thanks!

On Wed, Aug 14, 2013 at 1:14 AM, t x <txrev319 AT gmail.com> wrote:

Hi,

  What is happening at https://gist.github.com/anonymous/6227214#file-util-v-L342 ?

  In particular, I'm confused about:

  "(ls2 := t :: ls2)"

  The proof goes through on Coq -- so clearly it works and I'm in the wrong, but I don't understand what I'm misunderstanding. Here's what I know:

  (x: T)

  (ls2: list T)

  (ls1: list T)
 

  and I understand the Fixpoints/Theorems defined earlier in the file. However, I don't understand what is going on with:

  "(concat (ls2 := t :: ls2) tup1 (v, tup2))"

  In particular, the "ls2 := t :: ls2" part makes no sense to me:

  (1) how can this ever be satisfied?

  (2) why do make this assignment since ls2 isn't used anywhere else?

Thanks!