Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Forcing substitutions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Forcing substitutions


Chronological Thread 
  • From: t x <txrev319 AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Forcing substitutions
  • Date: Mon, 15 Jul 2013 23:05:26 -0700

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!



Archive powered by MHonArc 2.6.18.

Top of Page