1 files changed, 0 insertions, 55 deletions
diff --git a/src/Util/ForLoop/Tests.v b/src/Util/ForLoop/Tests.v
deleted file mode 100644
index 1061f1958..000000000
--- a/src/Util/ForLoop/Tests.v
+++ /dev/null
@@ -1,55 +0,0 @@
-Require Import Coq.ZArith.BinInt.
-Require Import Coq.micromega.Psatz.
-Require Import Crypto.Util.ForLoop.
-Require Import Crypto.Util.ForLoop.InvariantFramework.
-Require Import Crypto.Util.ZUtil.
-
-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) }}).
-
-Compute for (int i = 0; i < 5; i++) updating (v = 0) {{ v + i }}.
-Compute for (int i = 0; i <= 5; i++) updating (v = 0) {{ v + i }}.
-Compute for (int i = 5; i > -1; i--) updating (v = 0) {{ v + i }}.
-Compute for (int i = 5; i >= 0; i--) updating (v = 0) {{ v + i }}.
-Compute for (int i = 0; i < 5; i += 2) updating (v = 0) {{ v + i }}.
-Compute for (int i = 0; i <= 5; i += 2) updating (v = 0) {{ v + i }}.
-Compute for (int i = 5; i > -1; i -= 2) updating (v = 0) {{ v + i }}.
-Compute for (int i = 5; i >= 0; i -= 2) updating (v = 0) {{ v + i }}.
-Compute for (int i = 0; i < 6; i += 2) updating (v = 0) {{ v + i }}.
-Compute for (int i = 0; i <= 6; i += 2) updating (v = 0) {{ v + i }}.
-Compute for (int i = 6; i > -1; i -= 2) updating (v = 0) {{ v + i }}.
-Compute for (int i = 6; i >= 0; i -= 2) updating (v = 0) {{ v + i }}.
-Check eq_refl : for (int i = 0; i <= 5; i++) updating (v = 0) {{ v + i }} = 15.
-Check eq_refl : for (int i = 0; i < 5; i++) updating (v = 0) {{ v + i }} = 10.
-Check eq_refl : for (int i = 5; i >= 0; i--) updating (v = 0) {{ v + i }} = 15.
-Check eq_refl : for (int i = 5; i > -1; i--) updating (v = 0) {{ v + i }} = 15.
-Check eq_refl : for (int i = 0; i <= 5; i += 2) updating (v = 0) {{ v + i }} = 6.
-Check eq_refl : for (int i = 0; i < 5; i += 2) updating (v = 0) {{ v + i }} = 6.
-Check eq_refl : for (int i = 5; i > -1; i -= 2) updating (v = 0) {{ v + i }} = 9.
-Check eq_refl : for (int i = 5; i >= 0; i -= 2) updating (v = 0) {{ v + i }} = 9.
-Check eq_refl : for (int i = 0; i <= 6; i += 2) updating (v = 0) {{ v + i }} = 12.
-Check eq_refl : for (int i = 0; i < 6; i += 2) updating (v = 0) {{ v + i }} = 6.
-Check eq_refl : for (int i = 6; i > -1; i -= 2) updating (v = 0) {{ v + i }} = 12.
-Check eq_refl : for (int i = 6; i >= 0; i -= 2) updating (v = 0) {{ v + i }} = 12.
-
-Local Notation for_sumT n'
-  := (let n := Z.pos n' in
-      (2 *
-       for (int i = 0; i <= n; i++) updating (v = 0) {{
-         v + i
-       }})%Z
-      = n * (n + 1))
-       (only parsing).
-
-Check eq_refl : for_sumT 5.
-
-(** Here we show that if we add the numbers from 0 to n, we get [n * (n + 1) / 2] *)
-Example for_sum n' : for_sumT n'.
-Proof.
-  intro n.
-  apply for_loop_ind_le1.
-  { compute; reflexivity. }
-  { intros; nia. }
-Qed.