From 80ee8d2ea21ecfa83ec352a514bbfa9ae09e3f61 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 16 Jul 2016 18:02:37 +0200 Subject: Fixing #4932 (anomaly when using binders as terms in recursive notations). This application was actually not anticipated. It is nice and was not too difficult to support. Design for pattern binders maybe to clarify. When seing pat(x1,..,xn) as a term, I just reused pat(x1,..,xn), but maybe it is worth using the variable aliasing the pattern, for more a concise notation. But at the same time, this means exposing the internal name of the alias which is not so elegant. --- test-suite/bugs/closed/4932.v | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 test-suite/bugs/closed/4932.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/4932.v b/test-suite/bugs/closed/4932.v new file mode 100644 index 0000000000..df200cdce0 --- /dev/null +++ b/test-suite/bugs/closed/4932.v @@ -0,0 +1,40 @@ +(* 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. +Check test nat. + +Example test2 := tele (t : Type) (x:t) := tt. +Check test2 nat 0. + +Check tele (t : Type) (y:=0) (x:t) := tt. +Check (tele (t : Type) (y:=0) (x:t) := tt) nat 0. + +Check tele (t : Type) '((y,z):nat*nat) (x:t) := tt. +Check (tele (t : Type) '((y,z):nat*nat) (x:t) := tt) nat (1,2) 3. -- cgit v1.2.3