@@ 223,7 223,7 @@ primiera_score p: Player => Nat.
has_all_the_way_down? p: Player, s: Suit, r: Rank => Bool.
---
-captured? p s r <-> some c: Card ...
+captured? p s r <-> some c: Card ...
c in captures p and
suit c = s and
value c = r.
@@ 191,9 191,9 @@ then 8, 9, 10 for the courts.</p>
<br>
value c = case (rank c) …<br>
- "jack" ⇒ 8,<br>
- "queen" ⇒ 9,<br>
- "king" ⇒ 10,<br>
+ <i>jack</i> ⇒ 8,<br>
+ <i>queen</i> ⇒ 9,<br>
+ <i>king</i> ⇒ 10,<br>
 _ ⇒ rank c.<br>
<br>
match p c k → do<br>
@@ 304,23 304,23 @@ has-majority-cards? p ↔ #(captures p) > 20.<br>
has-majority-cards? p → score p 1.<br>
<br>
has-majority-diamonds? p ↔ <br>
- #{∀ c: Card, c in captures p, suit c = "diamonds" … c} > 5.<br>
+ #{∀ c: Card, c in captures p, suit c = <i>diamonds</i> … c} > 5.<br>
has-majority-diamonds? p → score p 1.<br>
<br>
-has-sette-bello? ↔ captured? p "diamonds" 7.<br>
+has-sette-bello? ↔ captured? p <i>diamonds</i> 7.<br>
has-sette-bello? p → score p 1.<br>
<br>
has-primiera? p ↔ ∀ other-p: Player, other-p ≠ p … <br>
 primiera-score p > primiera-score other-p.<br>
has-primiera? p → score p 1.<br>
<br>
-has-piccolo? p ↔ has-all-the-way-down? p "diamonds" 3.<br>
-has-piccolo? p → score p #{∀ r: Rank … has-all-the-way-down? p "diamonds" r}.<br>
+has-piccolo? p ↔ has-all-the-way-down? p <i>diamonds</i> 3.<br>
+has-piccolo? p → score p #{∀ r: Rank … has-all-the-way-down? p <i>diamonds</i> r}.<br>
<br>
has-grande? p ↔ <br>
- captured? p "diamonds" "jack" and<br>
- captured? p "diamonds" "queen" and<br>
- captured? p "diamonds" "king".<br>
+ captured? p <i>diamonds</i> <i>jack</i> and<br>
+ captured? p <i>diamonds</i> <i>queen</i> and<br>
+ captured? p <i>diamonds</i> <i>king</i>.<br>
<br>
<p class=where>where</p>
<br>
@@ 337,7 337,7 @@ primiera-score p: Player ⇒ ℕ.<br>
has-all-the-way-down? p: Player, s: Suit, r: Rank ⇒ 𝔹.<br>
<hr class=chapter-separator>
<br>
-captured? p s r ↔ ∃ c: Card … <br>
+captured? p s r ↔ ∃ c: Card …<br>
 c in captures p and <br>
 suit c = s and<br>
 value c = r.<br>
@@ 394,7 394,7 @@ round.</p>
<br>
(∃ p: Player …<br>
 scores p ≥ 51 or<br>
- #{∀ c: Card, c in captures p, suit c = "diamonds" … c} = 10)<br>
+ #{∀ c: Card, c in captures p, suit c = <i>diamonds</i> … c} = 10)<br>
 → win? p.<br>
<br>
</body>