The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

This solved my problem. Thanks again for all your help!

On Sat, Jun 1, 2013 at 12:24 AM, Yucheng Zhang <yczhang89 AT gmail.com> wrote:

On Jun 1, 2013, at 3:12 PM, Math Prover <mathprover AT gmail.com> wrote:
> Another stupid question from me:
>
> (1)  "magic n 10"
> (2)  "magic n (length (1::2::3::4::5::6::7::8::9::10::nil))"
>
> (1) works. (2) somehow does not work. Is there somewhat I can embed a simpl/compute/cbv somewhere so that "length (1::2::...::nil))" gets simplified to 10 before it hits ltac (or have ltac handle this case as well?)

After some digging into the Coq Reference Manual, I found out we can do this:

Ltac magic n k :=

  match eval compute in k with

    | O => idtac
    | S ?k' => destruct n; [ | magic n k' ]
  end.