Add regression test for github issue #133.

Renamed old "issue133" to "trac133", indicating that it uses a different
numbering system.

tests/issues/issue133.cry

@@ -1,5 +1,3 @@
-example1 : {a} (a >= 1, 2 >= a) => [16*a][8] -> [16][8]
-example1 k = drop`{16} ((zero : [16*(2 - a)][8]) #k)
-
-example2 : {a} (a >= 1, 2 >= a) => [16*a][8] -> [16][8]
-example2 k = drop`{16} (zero # k)
+gcd : [8] -> [8] -> [8]
+gcd a b = if(b == 0) then a
+          else gcd b (a%b)

tests/issues/issue133.icry

@@ -1,3 +1,3 @@
 :load issue133.cry
-:type example1
-:type example2
+:exhaust \x -> gcd 0 x == x
+:prove \x -> gcd 0 x == x

tests/issues/issue133.icry.stdout

@@ -1,5 +1,7 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module Main
-example1 : {a} (a >= 1, 2 >= a) => [16 * a][8] -> [16][8]
-example2 : {a} (a >= 1, 2 >= a) => [16 * a][8] -> [16][8]
+Using exhaustive testing.
+  0%  0%  0%  1%  1%  1%  2%  2%  3%  3%  3%  4%  4%  5%  5%  5%  6%  6%  7%  7%  7%  8%  8%  8%  9%  9% 10% 10% 10% 11% 11% 12% 12% 12% 13% 13% 14% 14% 14% 15% 15% 16% 16% 16% 17% 17% 17% 18% 18% 19% 19% 19% 20% 20% 21% 21% 21% 22% 22% 23% 23% 23% 24% 24% 25% 25% 25% 26% 26% 26% 27% 27% 28% 28% 28% 29% 29% 30% 30% 30% 31% 31% 32% 32% 32% 33% 33% 33% 34% 34% 35% 35% 35% 36% 36% 37% 37% 37% 38% 38% 39% 39% 39% 40% 40% 41% 41% 41% 42% 42% 42% 43% 43% 44% 44% 44% 45% 45% 46% 46% 46% 47% 47% 48% 48% 48% 49% 49% 50% 50% 50% 51% 51% 51% 52% 52% 53% 53% 53% 54% 54% 55% 55% 55% 56% 56% 57% 57% 57% 58% 58% 58% 59% 59% 60% 60% 60% 61% 61% 62% 62% 62% 63% 63% 64% 64% 64% 65% 65% 66% 66% 66% 67% 67% 67% 68% 68% 69% 69% 69% 70% 70% 71% 71% 71% 72% 72% 73% 73% 73% 74% 74% 75% 75% 75% 76% 76% 76% 77% 77% 78% 78% 78% 79% 79% 80% 80% 80% 81% 81% 82% 82% 82% 83% 83% 83% 84% 84% 85% 85% 85% 86% 86% 87% 87% 87% 88% 88% 89% 89% 89% 90% 90% 91% 91% 91% 92% 92% 92% 93% 93% 94% 94% 94% 95% 95% 96% 96% 96% 97% 97% 98% 98% 98% 99% 99%passed 256 tests.
+Q.E.D.
+Q.E.D.

tests/issues/trac133.cry

@@ -0,0 +1,5 @@
+example1 : {a} (a >= 1, 2 >= a) => [16*a][8] -> [16][8]
+example1 k = drop`{16} ((zero : [16*(2 - a)][8]) #k)
+
+example2 : {a} (a >= 1, 2 >= a) => [16*a][8] -> [16][8]
+example2 k = drop`{16} (zero # k)

tests/issues/trac133.icry

@@ -0,0 +1,3 @@
+:load trac133.cry
+:type example1
+:type example2

tests/issues/trac133.icry.stdout

@@ -0,0 +1,5 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+example1 : {a} (a >= 1, 2 >= a) => [16 * a][8] -> [16][8]
+example2 : {a} (a >= 1, 2 >= a) => [16 * a][8] -> [16][8]