The Coq mailing list

[t x <txrev319 AT gmail.com>]

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!