diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/bugs/closed/1925.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/bugs/closed/1925.v')
-rw-r--r-- | test-suite/bugs/closed/1925.v | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/1925.v b/test-suite/bugs/closed/1925.v new file mode 100644 index 00000000..4caee1c3 --- /dev/null +++ b/test-suite/bugs/closed/1925.v @@ -0,0 +1,22 @@ +(* Check that the analysis of projectable rel's in an evar instance is up to + aliases *) + +Require Import List. + +Definition compose (A B C : Type) (g : B -> C) (f : A -> B) : A -> C := + fun x : A => g(f x). + +Definition map_fuse' : + forall (A B C : Type) (g : B -> C) (f : A -> B) (xs : list A), + (map g (map f xs)) = map (compose _ _ _ g f) xs + := + fun A B C g f => + (fix loop (ys : list A) {struct ys} := + match ys as ys return (map g (map f ys)) = map (compose _ _ _ g f) ys + with + | nil => refl_equal nil + | x :: xs => + match loop xs in eq _ a return eq _ ((g (f x)) :: a) with + | refl_equal => refl_equal (map g (map f (x :: xs))) + end + end). |