diff options
| author | Hugo Herbelin | 2017-12-02 21:27:17 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-12-03 14:57:26 +0100 |
| commit | 594581601b2cc568f32c72b29d51d9d63da2879b (patch) | |
| tree | 74e98e83923da2341d2d7eda3281ab2b160c156a | |
| parent | 0048cbe810c82a775558c14cd7fcae644e205c51 (diff) | |
Adding a test for #6304 (bug with fix in notations).
| -rw-r--r-- | test-suite/output/Notations2.out | 6 | ||||
| -rw-r--r-- | test-suite/output/Notations2.v | 21 |
2 files changed, 27 insertions, 0 deletions
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 1ec701ae81..f57cc163d0 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -84,3 +84,9 @@ a≡ : Set .α : Set +# a : .α => +# b : .α => +let res := 0 in +for i from 0 to a updating (res) +{{for j from 0 to b updating (res) {{S res}};; res}};; res + : .α -> .α -> .α diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index ceb29d1b9e..9ca180c9df 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -145,3 +145,24 @@ Check .a≡. Notation ".α" := nat. Check nat. Check .α. + +(* A test for #6304 *) + +Module M6304. +Notation "'for' m 'from' 0 'to' N 'updating' ( s1 ) {{ b }} ;; rest" := + (let s1 := + (fix rec(n: nat) := match n with + | 0 => s1 + | S m => let s1 := rec m in b + end) N + in rest) + (at level 20). + +Check fun (a b : nat) => + let res := 0 in + for i from 0 to a updating (res) {{ + for j from 0 to b updating (res) {{ S res }};; + res + }};; res. + +End M6304. |