diff options
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 } |