The Coq mailing list

[t x <txrev319 AT gmail.com>]

(as an update, here's a minimal example)

https://gist.github.com/anonymous/0b02f3ad30e154515b87

the issue that is not clear to me is:

*) why is it not substituting?

*) how do I force a substitution?

On Mon, Jul 15, 2013 at 11:05 PM, t x <txrev319 AT gmail.com> wrote:

I have a goal that looks something like this:

==== BEGIN ====

None =

(fix z_nth_opt (lst : list K) (i0 : Z) {struct lst} : option K :=

   if i0 <? 0

   then None

   else

    match lst with

    | nil => None

    | x0 :: xs0 => if i0 =? 0 then Some x0 else z_nth_opt xs0 (i0 - 1)

    end) xs (i - 1)

==== END ====

I've tried "simpl/hnf" -- neither of which does anything.

I've also tried "cbv/compute", which expands the code _inside_ the fix, but does not substitute "into" the fix.

This is what I want:

  I want "xs" to be substitute in for lst. I want "(i-1)" to be substituted into as i0.

Question: how do I tell a "fix" to substitute in the args?

Thanks!