diff options
| author | Hannes Schulze <contact@haschu.me> | 2026-04-14 16:04:44 +0200 |
|---|---|---|
| committer | Hannes Schulze <contact@haschu.me> | 2026-04-15 13:22:40 +0200 |
| commit | a5ff8efe5b5e314e0aa759318e5fb194e066f612 (patch) | |
| tree | 4d13dd84ac4ced2360a51799f0e5c846bd733872 /Nominal/Helpers | |
| parent | 43942e78f4b3ed4cfca3b508f06161d0983c545e (diff) | |
update lean
Diffstat (limited to 'Nominal/Helpers')
| -rw-r--r-- | Nominal/Helpers/CountableString.lean | 6 |
1 files changed, 3 insertions, 3 deletions
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 } |