diff options
Diffstat (limited to 'test-suite/success/Notations2.v')
| -rw-r--r-- | test-suite/success/Notations2.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 9505a56e3..2655b651a 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -90,3 +90,18 @@ 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). + +(* 11. Notations with needed factorization of a recursive pattern *) +(* See https://github.com/coq/coq/issues/6078#issuecomment-342287412 *) +Module A. +Notation "[:: x1 ; .. ; xn & s ]" := (cons x1 .. (cons xn s) ..). +Notation "[:: x1 ; .. ; xn ]" := (cons x1 .. (cons xn nil) ..). +Check [:: 1 ; 2 ; 3 ]. +Check [:: 1 ; 2 ; 3 & nil ]. (* was failing *) +End A. |