The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

I think it's a type inference bug. I've reported a similar bug before. Try this instead:

Fixpoint dict_get (lst: dict K V) (k: K) {struct lst} : in_list k (keys lst) -> V.
refine(
match lst with
| nil => fun H => False_rect _ (lem__in_list_nil _ H)
| x :: xs => _
end).

On Wed, Aug 21, 2013 at 12:02 AM, t x <txrev319 AT gmail.com> wrote:

I'm trying to understand how to change functions from ": option X" to ": X" by passing along proofs.

However, in this example:

https://gist.github.com/anonymous/9f56cd467bc2e80c7d9c#file-test-v-L45

I get a stack overflow when I try to process lines 45-49. (Weirdly enough, if I change line 47 to:

| nil => fun H => _

then everything goes through fine.

What am I doing wrong?