coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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!
- [Coq-Club] Forcing substitutions, t x, 07/16/2013
- [Coq-Club] Re: Forcing substitutions, t x, 07/16/2013
- Re: [Coq-Club] Re: Forcing substitutions, Guillaume Melquiond, 07/16/2013
- Re: [Coq-Club] Re: Forcing substitutions, Duckki Oe, 07/18/2013
- Re: [Coq-Club] Re: Forcing substitutions, Duckki Oe, 07/18/2013
- [Coq-Club] Re: Forcing substitutions, t x, 07/16/2013
Archive powered by MHonArc 2.6.18.