From 1f0f5ebd05b00c02fb868eb94e96e7778513f108 Mon Sep 17 00:00:00 2001 From: Austin Letson Date: Tue, 7 May 2024 08:20:19 -0400 Subject: [PATCH] doc: fix typo Co-authored-by: David Thrane Christiansen --- src/Init/Data/String/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 0700a12cbb1b..01ee887e388e 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -180,7 +180,7 @@ the result is unspecified. Examples: * `"abc".next ⟨1⟩ = String.Pos.mk 2` * `"L∃∀N".next ⟨1⟩ = String.Pos.mk 4` -`'∃'` is a mutli-byte character +`'∃'` is a multi-byte character Cases where the result is unspecified: * `"abc".next ⟨3⟩`, since `3 = s.endPos`