@@ -6,63 +6,237 @@ open LeanTest
66def yachtTests : TestSuite :=
77 (TestSuite.empty "Yacht" )
88 |>.addTest "Yacht" (do
9- return assertEqual 50 (Yacht.score ⟨#[⟨5 , by decide⟩, ⟨5 , by decide⟩, ⟨5 , by decide⟩, ⟨5 , by decide⟩, ⟨5 , by decide⟩], by decide⟩ .yacht))
9+ return assertEqual 50 (Yacht.score ⟨#[
10+ ⟨5 , by decide⟩,
11+ ⟨5 , by decide⟩,
12+ ⟨5 , by decide⟩,
13+ ⟨5 , by decide⟩,
14+ ⟨5 , by decide⟩
15+ ], by decide⟩ .yacht))
1016 |>.addTest "Not Yacht" (do
11- return assertEqual 0 (Yacht.score ⟨#[⟨1 , by decide⟩, ⟨3 , by decide⟩, ⟨3 , by decide⟩, ⟨2 , by decide⟩, ⟨5 , by decide⟩], by decide⟩ .yacht))
17+ return assertEqual 0 (Yacht.score ⟨#[
18+ ⟨1 , by decide⟩,
19+ ⟨3 , by decide⟩,
20+ ⟨3 , by decide⟩,
21+ ⟨2 , by decide⟩,
22+ ⟨5 , by decide⟩
23+ ], by decide⟩ .yacht))
1224 |>.addTest "Ones" (do
13- return assertEqual 3 (Yacht.score ⟨#[⟨1 , by decide⟩, ⟨1 , by decide⟩, ⟨1 , by decide⟩, ⟨3 , by decide⟩, ⟨5 , by decide⟩], by decide⟩ .ones))
25+ return assertEqual 3 (Yacht.score ⟨#[
26+ ⟨1 , by decide⟩,
27+ ⟨1 , by decide⟩,
28+ ⟨1 , by decide⟩,
29+ ⟨3 , by decide⟩,
30+ ⟨5 , by decide⟩
31+ ], by decide⟩ .ones))
1432 |>.addTest "Ones, out of order" (do
15- return assertEqual 3 (Yacht.score ⟨#[⟨3 , by decide⟩, ⟨1 , by decide⟩, ⟨1 , by decide⟩, ⟨5 , by decide⟩, ⟨1 , by decide⟩], by decide⟩ .ones))
33+ return assertEqual 3 (Yacht.score ⟨#[
34+ ⟨3 , by decide⟩,
35+ ⟨1 , by decide⟩,
36+ ⟨1 , by decide⟩,
37+ ⟨5 , by decide⟩,
38+ ⟨1 , by decide⟩
39+ ], by decide⟩ .ones))
1640 |>.addTest "No ones" (do
17- return assertEqual 0 (Yacht.score ⟨#[⟨4 , by decide⟩, ⟨3 , by decide⟩, ⟨6 , by decide⟩, ⟨5 , by decide⟩, ⟨5 , by decide⟩], by decide⟩ .ones))
41+ return assertEqual 0 (Yacht.score ⟨#[
42+ ⟨4 , by decide⟩,
43+ ⟨3 , by decide⟩,
44+ ⟨6 , by decide⟩,
45+ ⟨5 , by decide⟩,
46+ ⟨5 , by decide⟩
47+ ], by decide⟩ .ones))
1848 |>.addTest "Twos" (do
19- return assertEqual 2 (Yacht.score ⟨#[⟨2 , by decide⟩, ⟨3 , by decide⟩, ⟨4 , by decide⟩, ⟨5 , by decide⟩, ⟨6 , by decide⟩], by decide⟩ .twos))
49+ return assertEqual 2 (Yacht.score ⟨#[
50+ ⟨2 , by decide⟩,
51+ ⟨3 , by decide⟩,
52+ ⟨4 , by decide⟩,
53+ ⟨5 , by decide⟩,
54+ ⟨6 , by decide⟩
55+ ], by decide⟩ .twos))
2056 |>.addTest "Fours" (do
21- return assertEqual 8 (Yacht.score ⟨#[⟨1 , by decide⟩, ⟨4 , by decide⟩, ⟨1 , by decide⟩, ⟨4 , by decide⟩, ⟨1 , by decide⟩], by decide⟩ .fours))
57+ return assertEqual 8 (Yacht.score ⟨#[
58+ ⟨1 , by decide⟩,
59+ ⟨4 , by decide⟩,
60+ ⟨1 , by decide⟩,
61+ ⟨4 , by decide⟩,
62+ ⟨1 , by decide⟩
63+ ], by decide⟩ .fours))
2264 |>.addTest "Yacht counted as threes" (do
23- return assertEqual 15 (Yacht.score ⟨#[⟨3 , by decide⟩, ⟨3 , by decide⟩, ⟨3 , by decide⟩, ⟨3 , by decide⟩, ⟨3 , by decide⟩], by decide⟩ .threes))
65+ return assertEqual 15 (Yacht.score ⟨#[
66+ ⟨3 , by decide⟩,
67+ ⟨3 , by decide⟩,
68+ ⟨3 , by decide⟩,
69+ ⟨3 , by decide⟩,
70+ ⟨3 , by decide⟩
71+ ], by decide⟩ .threes))
2472 |>.addTest "Yacht of 3s counted as fives" (do
25- return assertEqual 0 (Yacht.score ⟨#[⟨3 , by decide⟩, ⟨3 , by decide⟩, ⟨3 , by decide⟩, ⟨3 , by decide⟩, ⟨3 , by decide⟩], by decide⟩ .fives))
73+ return assertEqual 0 (Yacht.score ⟨#[
74+ ⟨3 , by decide⟩,
75+ ⟨3 , by decide⟩,
76+ ⟨3 , by decide⟩,
77+ ⟨3 , by decide⟩,
78+ ⟨3 , by decide⟩
79+ ], by decide⟩ .fives))
2680 |>.addTest "Fives" (do
27- return assertEqual 10 (Yacht.score ⟨#[⟨1 , by decide⟩, ⟨5 , by decide⟩, ⟨3 , by decide⟩, ⟨5 , by decide⟩, ⟨3 , by decide⟩], by decide⟩ .fives))
81+ return assertEqual 10 (Yacht.score ⟨#[
82+ ⟨1 , by decide⟩,
83+ ⟨5 , by decide⟩,
84+ ⟨3 , by decide⟩,
85+ ⟨5 , by decide⟩,
86+ ⟨3 , by decide⟩
87+ ], by decide⟩ .fives))
2888 |>.addTest "Sixes" (do
29- return assertEqual 6 (Yacht.score ⟨#[⟨2 , by decide⟩, ⟨3 , by decide⟩, ⟨4 , by decide⟩, ⟨5 , by decide⟩, ⟨6 , by decide⟩], by decide⟩ .sixes))
89+ return assertEqual 6 (Yacht.score ⟨#[
90+ ⟨2 , by decide⟩,
91+ ⟨3 , by decide⟩,
92+ ⟨4 , by decide⟩,
93+ ⟨5 , by decide⟩,
94+ ⟨6 , by decide⟩
95+ ], by decide⟩ .sixes))
3096 |>.addTest "Full house two small, three big" (do
31- return assertEqual 16 (Yacht.score ⟨#[⟨2 , by decide⟩, ⟨2 , by decide⟩, ⟨4 , by decide⟩, ⟨4 , by decide⟩, ⟨4 , by decide⟩], by decide⟩ .fullHouse))
97+ return assertEqual 16 (Yacht.score ⟨#[
98+ ⟨2 , by decide⟩,
99+ ⟨2 , by decide⟩,
100+ ⟨4 , by decide⟩,
101+ ⟨4 , by decide⟩,
102+ ⟨4 , by decide⟩
103+ ], by decide⟩ .fullHouse))
32104 |>.addTest "Full house three small, two big" (do
33- return assertEqual 19 (Yacht.score ⟨#[⟨5 , by decide⟩, ⟨3 , by decide⟩, ⟨3 , by decide⟩, ⟨5 , by decide⟩, ⟨3 , by decide⟩], by decide⟩ .fullHouse))
105+ return assertEqual 19 (Yacht.score ⟨#[
106+ ⟨5 , by decide⟩,
107+ ⟨3 , by decide⟩,
108+ ⟨3 , by decide⟩,
109+ ⟨5 , by decide⟩,
110+ ⟨3 , by decide⟩
111+ ], by decide⟩ .fullHouse))
34112 |>.addTest "Two pair is not a full house" (do
35- return assertEqual 0 (Yacht.score ⟨#[⟨2 , by decide⟩, ⟨2 , by decide⟩, ⟨4 , by decide⟩, ⟨4 , by decide⟩, ⟨5 , by decide⟩], by decide⟩ .fullHouse))
113+ return assertEqual 0 (Yacht.score ⟨#[
114+ ⟨2 , by decide⟩,
115+ ⟨2 , by decide⟩,
116+ ⟨4 , by decide⟩,
117+ ⟨4 , by decide⟩,
118+ ⟨5 , by decide⟩
119+ ], by decide⟩ .fullHouse))
36120 |>.addTest "Four of a kind is not a full house" (do
37- return assertEqual 0 (Yacht.score ⟨#[⟨1 , by decide⟩, ⟨4 , by decide⟩, ⟨4 , by decide⟩, ⟨4 , by decide⟩, ⟨4 , by decide⟩], by decide⟩ .fullHouse))
121+ return assertEqual 0 (Yacht.score ⟨#[
122+ ⟨1 , by decide⟩,
123+ ⟨4 , by decide⟩,
124+ ⟨4 , by decide⟩,
125+ ⟨4 , by decide⟩,
126+ ⟨4 , by decide⟩
127+ ], by decide⟩ .fullHouse))
38128 |>.addTest "Yacht is not a full house" (do
39- return assertEqual 0 (Yacht.score ⟨#[⟨2 , by decide⟩, ⟨2 , by decide⟩, ⟨2 , by decide⟩, ⟨2 , by decide⟩, ⟨2 , by decide⟩], by decide⟩ .fullHouse))
129+ return assertEqual 0 (Yacht.score ⟨#[
130+ ⟨2 , by decide⟩,
131+ ⟨2 , by decide⟩,
132+ ⟨2 , by decide⟩,
133+ ⟨2 , by decide⟩,
134+ ⟨2 , by decide⟩
135+ ], by decide⟩ .fullHouse))
40136 |>.addTest "Four of a Kind" (do
41- return assertEqual 24 (Yacht.score ⟨#[⟨6 , by decide⟩, ⟨6 , by decide⟩, ⟨4 , by decide⟩, ⟨6 , by decide⟩, ⟨6 , by decide⟩], by decide⟩ .fourOfAKind))
137+ return assertEqual 24 (Yacht.score ⟨#[
138+ ⟨6 , by decide⟩,
139+ ⟨6 , by decide⟩,
140+ ⟨4 , by decide⟩,
141+ ⟨6 , by decide⟩,
142+ ⟨6 , by decide⟩
143+ ], by decide⟩ .fourOfAKind))
42144 |>.addTest "Yacht can be scored as Four of a Kind" (do
43- return assertEqual 12 (Yacht.score ⟨#[⟨3 , by decide⟩, ⟨3 , by decide⟩, ⟨3 , by decide⟩, ⟨3 , by decide⟩, ⟨3 , by decide⟩], by decide⟩ .fourOfAKind))
145+ return assertEqual 12 (Yacht.score ⟨#[
146+ ⟨3 , by decide⟩,
147+ ⟨3 , by decide⟩,
148+ ⟨3 , by decide⟩,
149+ ⟨3 , by decide⟩,
150+ ⟨3 , by decide⟩
151+ ], by decide⟩ .fourOfAKind))
44152 |>.addTest "Full house is not Four of a Kind" (do
45- return assertEqual 0 (Yacht.score ⟨#[⟨3 , by decide⟩, ⟨3 , by decide⟩, ⟨3 , by decide⟩, ⟨5 , by decide⟩, ⟨5 , by decide⟩], by decide⟩ .fourOfAKind))
153+ return assertEqual 0 (Yacht.score ⟨#[
154+ ⟨3 , by decide⟩,
155+ ⟨3 , by decide⟩,
156+ ⟨3 , by decide⟩,
157+ ⟨5 , by decide⟩,
158+ ⟨5 , by decide⟩
159+ ], by decide⟩ .fourOfAKind))
46160 |>.addTest "Little Straight" (do
47- return assertEqual 30 (Yacht.score ⟨#[⟨3 , by decide⟩, ⟨5 , by decide⟩, ⟨4 , by decide⟩, ⟨1 , by decide⟩, ⟨2 , by decide⟩], by decide⟩ .littleStraight))
161+ return assertEqual 30 (Yacht.score ⟨#[
162+ ⟨3 , by decide⟩,
163+ ⟨5 , by decide⟩,
164+ ⟨4 , by decide⟩,
165+ ⟨1 , by decide⟩,
166+ ⟨2 , by decide⟩
167+ ], by decide⟩ .littleStraight))
48168 |>.addTest "Little Straight as Big Straight" (do
49- return assertEqual 0 (Yacht.score ⟨#[⟨1 , by decide⟩, ⟨2 , by decide⟩, ⟨3 , by decide⟩, ⟨4 , by decide⟩, ⟨5 , by decide⟩], by decide⟩ .bigStraight))
169+ return assertEqual 0 (Yacht.score ⟨#[
170+ ⟨1 , by decide⟩,
171+ ⟨2 , by decide⟩,
172+ ⟨3 , by decide⟩,
173+ ⟨4 , by decide⟩,
174+ ⟨5 , by decide⟩
175+ ], by decide⟩ .bigStraight))
50176 |>.addTest "Four in order but not a little straight" (do
51- return assertEqual 0 (Yacht.score ⟨#[⟨1 , by decide⟩, ⟨1 , by decide⟩, ⟨2 , by decide⟩, ⟨3 , by decide⟩, ⟨4 , by decide⟩], by decide⟩ .littleStraight))
177+ return assertEqual 0 (Yacht.score ⟨#[
178+ ⟨1 , by decide⟩,
179+ ⟨1 , by decide⟩,
180+ ⟨2 , by decide⟩,
181+ ⟨3 , by decide⟩,
182+ ⟨4 , by decide⟩
183+ ], by decide⟩ .littleStraight))
52184 |>.addTest "No pairs but not a little straight" (do
53- return assertEqual 0 (Yacht.score ⟨#[⟨1 , by decide⟩, ⟨2 , by decide⟩, ⟨3 , by decide⟩, ⟨4 , by decide⟩, ⟨6 , by decide⟩], by decide⟩ .littleStraight))
185+ return assertEqual 0 (Yacht.score ⟨#[
186+ ⟨1 , by decide⟩,
187+ ⟨2 , by decide⟩,
188+ ⟨3 , by decide⟩,
189+ ⟨4 , by decide⟩,
190+ ⟨6 , by decide⟩
191+ ], by decide⟩ .littleStraight))
54192 |>.addTest "Minimum is 1, maximum is 5, but not a little straight" (do
55- return assertEqual 0 (Yacht.score ⟨#[⟨1 , by decide⟩, ⟨1 , by decide⟩, ⟨3 , by decide⟩, ⟨4 , by decide⟩, ⟨5 , by decide⟩], by decide⟩ .littleStraight))
193+ return assertEqual 0 (Yacht.score ⟨#[
194+ ⟨1 , by decide⟩,
195+ ⟨1 , by decide⟩,
196+ ⟨3 , by decide⟩,
197+ ⟨4 , by decide⟩,
198+ ⟨5 , by decide⟩
199+ ], by decide⟩ .littleStraight))
56200 |>.addTest "Big Straight" (do
57- return assertEqual 30 (Yacht.score ⟨#[⟨4 , by decide⟩, ⟨6 , by decide⟩, ⟨2 , by decide⟩, ⟨5 , by decide⟩, ⟨3 , by decide⟩], by decide⟩ .bigStraight))
201+ return assertEqual 30 (Yacht.score ⟨#[
202+ ⟨4 , by decide⟩,
203+ ⟨6 , by decide⟩,
204+ ⟨2 , by decide⟩,
205+ ⟨5 , by decide⟩,
206+ ⟨3 , by decide⟩
207+ ], by decide⟩ .bigStraight))
58208 |>.addTest "Big Straight as little straight" (do
59- return assertEqual 0 (Yacht.score ⟨#[⟨6 , by decide⟩, ⟨5 , by decide⟩, ⟨4 , by decide⟩, ⟨3 , by decide⟩, ⟨2 , by decide⟩], by decide⟩ .littleStraight))
209+ return assertEqual 0 (Yacht.score ⟨#[
210+ ⟨6 , by decide⟩,
211+ ⟨5 , by decide⟩,
212+ ⟨4 , by decide⟩,
213+ ⟨3 , by decide⟩,
214+ ⟨2 , by decide⟩
215+ ], by decide⟩ .littleStraight))
60216 |>.addTest "No pairs but not a big straight" (do
61- return assertEqual 0 (Yacht.score ⟨#[⟨6 , by decide⟩, ⟨5 , by decide⟩, ⟨4 , by decide⟩, ⟨3 , by decide⟩, ⟨1 , by decide⟩], by decide⟩ .bigStraight))
217+ return assertEqual 0 (Yacht.score ⟨#[
218+ ⟨6 , by decide⟩,
219+ ⟨5 , by decide⟩,
220+ ⟨4 , by decide⟩,
221+ ⟨3 , by decide⟩,
222+ ⟨1 , by decide⟩
223+ ], by decide⟩ .bigStraight))
62224 |>.addTest "Choice" (do
63- return assertEqual 23 (Yacht.score ⟨#[⟨3 , by decide⟩, ⟨3 , by decide⟩, ⟨5 , by decide⟩, ⟨6 , by decide⟩, ⟨6 , by decide⟩], by decide⟩ .choice))
225+ return assertEqual 23 (Yacht.score ⟨#[
226+ ⟨3 , by decide⟩,
227+ ⟨3 , by decide⟩,
228+ ⟨5 , by decide⟩,
229+ ⟨6 , by decide⟩,
230+ ⟨6 , by decide⟩
231+ ], by decide⟩ .choice))
64232 |>.addTest "Yacht as choice" (do
65- return assertEqual 10 (Yacht.score ⟨#[⟨2 , by decide⟩, ⟨2 , by decide⟩, ⟨2 , by decide⟩, ⟨2 , by decide⟩, ⟨2 , by decide⟩], by decide⟩ .choice))
233+ return assertEqual 10 (Yacht.score ⟨#[
234+ ⟨2 , by decide⟩,
235+ ⟨2 , by decide⟩,
236+ ⟨2 , by decide⟩,
237+ ⟨2 , by decide⟩,
238+ ⟨2 , by decide⟩
239+ ], by decide⟩ .choice))
66240
67241def main : IO UInt32 := do
68242 runTestSuitesWithExitCode [yachtTests]
0 commit comments