The Coq mailing list

[S3 <scubed2 AT gmail.com>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

(*
Rewrite doesn't match, even though the forms look the same.
Why isn't it accepted?  How do they differ?
I tried "Set Printing All", but that didn't reveal any
hidden Set vs. Type differences.
I'm using Coq 8.3pl1 (July 2011).
*)

Require Import ZArith.

(* Iteratively call a function on itself p times. *)
Definition Repeat {A} (p : positive) (f : A -> A) (a : A) : A :=
  Prect (fun _ => A) (f a) (fun _ IHp => f IHp) p
.

(*
Theorem Repeat_eq A p f (a : A) : Repeat p f a =
  match p with
  | xH => f a
  | _ => f (Repeat (Ppred p) f a)
  end
.
  destruct p.
      change (Repeat p~1 f a =
        (let a0 := fun _ => A in
         let a1 := f a in
         let a2 := fun _ IHp => f IHp in
         let a3 := Ppred p~1 in
         a2 a3 (Prect a0 a1 a2 a3))).
      rewrite <- Prect_succ.

> rewrite <- Prect_succ. ^^^^^^^^^^^^^^^^^^^^^
Error:
Found no subterm matching "?72 ?73 (Prect ?70 ?71 ?72 ?73)" in the current 
goal.
*)

- -- 
echo 'scale=2735;sqrt(57)' | BC_LINE_LENGTH=391 bc |
tail -n 1 | tr 0-9 'ertiSSngl '
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.19 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://www.enigmail.net/

iEYEARECAAYFAlC8O+AACgkQxzVgPqtIcftqOgCfeF408hFKa9Qo0vfyGog0/5j0
FR4Anj7/Sg83FXVa2YlAPuchahloAxUe
=0KRL
-----END PGP SIGNATURE-----