From e02ad2dcc0f93107c18f8316b386b92b45548e97 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Sun, 30 Nov 2025 22:20:35 +0100 Subject: update lean --- Nominal/Helpers/CountableString.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'Nominal/Helpers') diff --git a/Nominal/Helpers/CountableString.lean b/Nominal/Helpers/CountableString.lean index 7d2fcb7..7d94516 100644 --- a/Nominal/Helpers/CountableString.lean +++ b/Nominal/Helpers/CountableString.lean @@ -9,4 +9,6 @@ instance : Countable Char where instance : Countable String := Countable.of_equiv (List Char) { toFun := String.mk - invFun := String.data } + invFun := String.data + left_inv x := by simp + right_inv x := by simp } -- cgit v1.3.1