diff options
Diffstat (limited to 'test-suite/bugs/opened/3510.v')
| -rw-r--r-- | test-suite/bugs/opened/3510.v | 35 |
1 files changed, 0 insertions, 35 deletions
diff --git a/test-suite/bugs/opened/3510.v b/test-suite/bugs/opened/3510.v deleted file mode 100644 index daf26507..00000000 --- a/test-suite/bugs/opened/3510.v +++ /dev/null @@ -1,35 +0,0 @@ -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. |