diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-14 18:14:39 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-14 18:14:39 -0400 |
| commit | e3d27bfc58b601d4c3f344670ce7d04597ac5e61 (patch) | |
| tree | 2a6a3c5f974bd5ac5f9efe4f4e5fb4605d84ec46 /src/Util/ForLoop | |
| parent | 8dc2c5c001b9b0e63ecf8324969b603694486d8b (diff) | |
Add for-loop combinator
Diffstat (limited to 'src/Util/ForLoop')
| -rw-r--r-- | src/Util/ForLoop/Tests.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Util/ForLoop/Tests.v b/src/Util/ForLoop/Tests.v new file mode 100644 index 000000000..7b800ddbc --- /dev/null +++ b/src/Util/ForLoop/Tests.v @@ -0,0 +1,7 @@ +Require Import Coq.ZArith.BinInt. +Require Import Crypto.Util.ForLoop. + +Local Open Scope Z_scope. + +Check (for i (:= 0; += 1; < 10) updating (v := 5) {{ v + i }}). +Check (for (int i = 0; i < 5; i++) updating ( '(v1, v2) = (0, 0) ) {{ (v1 + i, v2 + i) }}). |