diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /test-suite/bugs/closed/4216.v | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'test-suite/bugs/closed/4216.v')
-rw-r--r-- | test-suite/bugs/closed/4216.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4216.v b/test-suite/bugs/closed/4216.v new file mode 100644 index 00000000..ae7f7467 --- /dev/null +++ b/test-suite/bugs/closed/4216.v @@ -0,0 +1,20 @@ +Generalizable Variables T A. + +Inductive path `(a: A): A -> Type := idpath: path a a. + +Class TMonad (T: Type -> Type) := { + bind: forall {A B: Type}, (T A) -> (A -> T B) -> T B; + ret: forall {A: Type}, A -> T A; + ret_unit_left: forall {A B: Type} (k: A -> T B) (a: A), + path (bind (ret a) k) (k a) + }. + +Let T_fzip `{TMonad T} := fun (A B: Type) (f: T (A -> B)) (t: T A) + => bind t (fun a => bind f (fun g => ret (g a) )). +Let T_pure `{TMonad T} := @ret _ _. + +Let T_pure_id `{TMonad T} {A: Type} (t: A -> A) (x: T A): + path (T_fzip A A (T_pure (A -> A) t) x) x. + unfold T_fzip, T_pure. + Fail rewrite (ret_unit_left (fun g a => ret (g a)) (fun x => x)). + |