diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-07-28 13:47:39 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-07-28 13:47:39 +0200 |
commit | 3bdadb4020c1d3e51957a06c1e3a52744f09148d (patch) | |
tree | 4236eaa3d1858de16882223fd2eabeb30216c44d /test-suite/bugs/closed/3510.v | |
parent | 86e2b0ab9da7dbd9c4c39ab2ab8df05d94a42056 (diff) |
Tests for bugs #3509 and #3510.
Diffstat (limited to 'test-suite/bugs/closed/3510.v')
-rw-r--r-- | test-suite/bugs/closed/3510.v | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3510.v b/test-suite/bugs/closed/3510.v new file mode 100644 index 000000000..daf265071 --- /dev/null +++ b/test-suite/bugs/closed/3510.v @@ -0,0 +1,35 @@ +Require Import TestSuite.admit. +Lemma match_option_fn T (b : option T) A B s n +: match b as b return forall x : A, B b x with + | Some k => s k + | None => n + end + = fun x : A => match b as b return B b x with + | Some k => s k x + | None => n x + end. +admit. +Defined. +Lemma match_option_comm_2 T (p : option T) A B R (f : forall (x : A) (y : B x), R x y) (s1 : T -> A) (s2 : forall x : T, B (s1 x)) n1 n2 +: match p as p return R match p with + | Some k => s1 k + | None => n1 + end + match p as p return B match p with Some k => s1 k | None => n1 end with + | Some k => s2 k + | None => n2 + end with + | Some k => f (s1 k) (s2 k) + | None => f n1 n2 + end + = f match p return A with + | Some k => s1 k + | None => n1 + end + match p as p return B match p with Some k => s1 k | None => n1 end with + | Some k => s2 k + | None => n2 + end. +admit. +Defined. +Fail Hint Rewrite match_option_fn match_option_comm_2 : matchdb. |