diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-05 09:58:42 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-05 09:58:42 +0100 |
| commit | 4d62482e8c996024fdcdee1549bb8bfe28961763 (patch) | |
| tree | 43d0f5410df2a69f7e8f64311a76601f25eb12e6 /test-suite | |
| parent | 3e71e1961aae51b71a16ef0afe2a4473060f24ec (diff) | |
| parent | 594581601b2cc568f32c72b29d51d9d63da2879b (diff) | |
Merge PR #6306: Adding a test for #6304 (a bug with "fix" in notations).
Diffstat (limited to 'test-suite')
| -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 1ec701ae8..f57cc163d 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 ceb29d1b9..9ca180c9d 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. |