From a5ff8efe5b5e314e0aa759318e5fb194e066f612 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <contact@haschu.me>
Date: Tue, 14 Apr 2026 16:04:44 +0200
Subject: update lean

---
 Nominal/Helpers/CountableString.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'Nominal/Helpers/CountableString.lean')

diff --git a/Nominal/Helpers/CountableString.lean b/Nominal/Helpers/CountableString.lean
index b6f59f8..c887f96 100644
--- a/Nominal/Helpers/CountableString.lean
+++ b/Nominal/Helpers/CountableString.lean
@@ -5,10 +5,10 @@ instance : Countable Char where
     use Char.toNat
     intro c₁ c₂ hc
     rw [Char.toNat, Char.toNat, UInt32.toNat_inj] at hc
-    exact Char.eq_of_val_eq hc
+    exact Char.ext hc
 
 instance : Countable String := Countable.of_equiv (List Char)
-  { toFun := String.mk
-    invFun := String.data
+  { toFun := String.ofList
+    invFun := String.toList
     left_inv x := by simp
     right_inv x := by simp }
-- 
cgit v1.3.1