diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-08 19:58:41 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-14 00:34:51 +0100 |
| commit | 685643098eeef00fe1f8dfca0927db2e812e1e7a (patch) | |
| tree | b1e06399a7bf065bbe51c0d2fac2fee081e91a78 /test-suite/success/Notations2.v | |
| parent | ac76f1f2bf819a5999cef642f17652320f39fd80 (diff) | |
One more step in fixing #5762 ("where" clause).
We improve one step further the heuristics to sort out if a variable
is a notation variable or a named variable.
This allows to support the following which was still failing.
Reserved Notation "# x" (at level 0).
Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I).
We rely here on the property that a binding variable of same name as a
notation variables is itself considered bound by the notation.
This becomes however to be a bit tricky for sorting out if the
variable has to be output to the glob file or not.
Diffstat (limited to 'test-suite/success/Notations2.v')
| -rw-r--r-- | test-suite/success/Notations2.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 9505a56e3..e86b3edb8 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -90,3 +90,9 @@ Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end. Notation "##### x" := (pair' x) (at level 0, x at level 1). Check ##### 0 _ 0%bool 0%bool : prod' bool bool. Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end. + +(* 10. Check computation of binding variable through other notations *) +(* i should be detected as binding variable and the scopes not being checked *) + +Notation "'FUNNAT' i => t" := (fun i : nat => i = t) (at level 200). +Notation "'Funnat' i => t" := (FUNNAT i => t + i%nat) (at level 200). |