From 6c241c4e76a733d7950d39d296e85fe0f19346f6 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 28 Jul 2024 14:31:11 +1000
Subject: [PATCH] fix test

---
 tests/lean/run/starsAndBars.lean | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/tests/lean/run/starsAndBars.lean b/tests/lean/run/starsAndBars.lean
index 7c09693e5448..c39eb2966692 100644
--- a/tests/lean/run/starsAndBars.lean
+++ b/tests/lean/run/starsAndBars.lean
@@ -1,3 +1,7 @@
+@[simp] def List.count' [DecidableEq α] : List α → α → Nat
+  | [], _    => 0
+  | a::as, b => if a = b then as.count' b + 1 else as.count' b
+
 inductive StarsAndBars : Nat → Nat → Type where
   | nil  : StarsAndBars 0 0
   | star : StarsAndBars s b → StarsAndBars (s+1) b
@@ -7,7 +11,7 @@ namespace StarsAndBars
 
 namespace Ex1
 
-def toList : StarsAndBars s b → { bs : List Bool // bs.count false = s ∧ bs.count true = b }
+def toList : StarsAndBars s b → { bs : List Bool // bs.count' false = s ∧ bs.count' true = b }
   | nil    => ⟨[], by simp⟩
   | star h => ⟨false :: toList h, by simp [(toList h).2]⟩
   | bar  h => ⟨true :: toList h, by simp [(toList h).2]⟩
@@ -23,13 +27,13 @@ end Ex1
 /- Same example with explicit proofs -/
 namespace Ex2
 
-theorem toList_star_proof (h : bs.count false = s ∧ bs.count true = b) : (false :: bs).count false = s.succ ∧ (false :: bs).count true = b := by
+theorem toList_star_proof (h : bs.count' false = s ∧ bs.count' true = b) : (false :: bs).count' false = s.succ ∧ (false :: bs).count' true = b := by
   simp [*]
 
-theorem toList_bar_proof (h : bs.count false = s ∧ bs.count true = b) : (true :: bs).count false = s ∧ (true :: bs).count true = b.succ := by
+theorem toList_bar_proof (h : bs.count' false = s ∧ bs.count' true = b) : (true :: bs).count' false = s ∧ (true :: bs).count' true = b.succ := by
   simp [*]
 
-def toList : StarsAndBars s b → { bs : List Bool // bs.count false = s ∧ bs.count true = b }
+def toList : StarsAndBars s b → { bs : List Bool // bs.count' false = s ∧ bs.count' true = b }
   | nil    => ⟨[], by simp⟩
   | star h => ⟨false :: toList h, toList_star_proof (toList h).property⟩
   | bar  h => ⟨true :: toList h,  toList_bar_proof (toList h).property⟩