From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- test-suite/bugs/closed/4932.v | 44 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) create mode 100644 test-suite/bugs/closed/4932.v (limited to 'test-suite/bugs/closed/4932.v') diff --git a/test-suite/bugs/closed/4932.v b/test-suite/bugs/closed/4932.v new file mode 100644 index 00000000..219d532a --- /dev/null +++ b/test-suite/bugs/closed/4932.v @@ -0,0 +1,44 @@ +(* Testing recursive notations with binders seen as terms *) + +Inductive ftele : Type := +| fb {T:Type} : T -> ftele +| fr {T} : (T -> ftele) -> ftele. + +Fixpoint args ftele : Type := + match ftele with + | fb _ => unit + | fr f => sigT (fun t => args (f t)) + end. + +Definition fpack := sigT args. +Definition pack fp fa : fpack := existT _ fp fa. + +Notation "'tele' x .. z := b" := + ( + (fun x => .. + (fun z => + pack + (fr (fun x => .. ( fr (fun z => fb b) ) .. ) ) + (existT _ x .. (existT _ z tt) .. ) + ) .. + ) + ) (at level 85, x binder, z binder). + +Check fun '((y,z):nat*nat) => pack (fr (fun '((y,z):nat*nat) => fb tt)) + (existT _ (y,z) tt). + +Example test := tele (t : Type) := tt. +Example test' := test nat. +Print test. + +Example test2 := tele (t : Type) (x:t) := tt. +Example test2' := test2 nat 0. +Print test2. + +Example test3 := tele (t : Type) (y:=0) (x:t) := tt. +Example test3' := test3 nat 0. +Print test3. + +Example test4 := tele (t : Type) '((y,z):nat*nat) (x:t) := tt. +Example test4' := test4 nat (1,2) 3. +Print test4. -- cgit v1.2.3