Put the speed testing back.

example/omega1s1-wip.red

@@ -42,3 +42,28 @@ let winding-loopn (n : int) : Path int (winding (loopn n)) n =
     | suc (n ⇒ loopn) ⇒ λ i → pred (loopn i)
     ]
   ]
+
+
+; speed test
+
+let two : int = pos (suc (suc zero))
+
+let winding-loop-testing0 : Path int two (winding (loopn two)) =
+  auto
+
+let nat/five : nat =
+  suc (suc (suc (suc (suc zero))))
+
+let nat/25 : nat =
+  plus nat/five (plus nat/five (plus nat/five (plus nat/five nat/five)))
+
+let int/50 : int =
+  pos (plus nat/25 nat/25)
+
+let int/5 : int = pos nat/five
+
+let winding-test/5 : Path int int/5 (winding (loopn int/5)) =
+  auto
+
+let winding-test/50 : Path int int/50 (winding (loopn int/50)) =
+  auto