diff options
author | 2017-12-02 21:27:17 +0100 | |
---|---|---|
committer | 2017-12-03 14:57:26 +0100 | |
commit | 594581601b2cc568f32c72b29d51d9d63da2879b (patch) | |
tree | 74e98e83923da2341d2d7eda3281ab2b160c156a /test-suite/output/Notations2.v | |
parent | 0048cbe810c82a775558c14cd7fcae644e205c51 (diff) |
Adding a test for #6304 (bug with fix in notations).
Diffstat (limited to 'test-suite/output/Notations2.v')
-rw-r--r-- | test-suite/output/Notations2.v | 21 |
1 files changed, 21 insertions, 0 deletions
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. |