max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: simplify Char.toString to String.singleton (#12449)

Browse source 
This PR marks `String.toString_eq_singleton` as a `simp` lemma.
This commit is contained in:
Markus Himmel 2026-02-12 07:10:36 +01:00 • committed by GitHub
parent 9073ad37bb
commit 7b29425361
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Init/Data/Char/Lemmas.lean
View file

@ -83,6 +83,7 @@ def notLTTotal : Std.Total (¬ · < · : Char → Char → Prop) where
@[simp]
theorem toUInt8_val {c : Char} : c.val.toUInt8 = c.toUInt8 := rfl
@[simp]
theorem toString_eq_singleton {c : Char} : c.toString = String.singleton c := rfl
end Char

5
src/Init/Data/String/Basic.lean
View file

@ -3085,7 +3085,8 @@ end String
namespace Char
@[simp] theorem length_toString (c : Char) : c.toString.length = 1 := by
simp [toString_eq_singleton]
@[deprecated String.length_singleton (since := "2026-02-12")]
theorem length_toString (c : Char) : c.toString.length = 1 := by
simp
end Char