The Coq mailing list

[t x <txrev319 AT gmail.com>]

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!