Init.Data.String.Bootstrap

source

@[reducible, inline, deprecated String.Pos.Raw (since := "2025-09-30")]

abbrev String.Pos :

Type

Equations

String.Pos = String.Pos.Raw

Instances For

source

instance String.instOfNatRaw :

OfNat Pos.Raw 0

Equations

String.instOfNatRaw = { ofNat := { } }

source

instance String.instInhabited :

Inhabited String

Equations

String.instInhabited = { default := "" }

source

@[extern lean_string_push]

def String.push :

String → Char → String

Adds a character to the end of a string.

The internal implementation uses dynamic arrays and will perform destructive updates if the string is not shared.

Examples:

"abc".push 'd' = "abcd"
"".push 'a' = "a"

Equations

x✝¹.push x✝ = match x✝¹, x✝ with | { bytes := b, isValidUTF8 := h }, c => { bytes := b.append [c].utf8Encode, isValidUTF8 := ⋯ }

Instances For

source

@[inline]

def String.singleton (c : Char) :

String

Returns a new string that contains only the character c.

Because strings are encoded in UTF-8, the resulting string may take multiple bytes.

Examples:

String.singleton 'L' = "L"
String.singleton ' ' = " "
String.singleton '"' = "\""
String.singleton '𝒫' = "𝒫"

Equations

String.singleton c = "".push c

Instances For

source

@[extern lean_string_posof]

opaque String.Internal.posOf (s : String) (c : Char) :

Pos.Raw

source

@[extern lean_string_offsetofpos]

opaque String.Internal.offsetOfPos (s : String) (pos : Pos.Raw) :

Nat

source

@[extern lean_string_utf8_extract]

opaque String.Internal.extract :

String → Pos.Raw → Pos.Raw → String

source

@[extern lean_string_length]

opaque String.Internal.length :

String → Nat

source

@[extern lean_string_pushn]

opaque String.Internal.pushn (s : String) (c : Char) (n : Nat) :

String

source

@[extern lean_string_append]

opaque String.Internal.append :

String → String → String

source

@[extern lean_string_utf8_next]

opaque String.Internal.next (s : String) (p : Pos.Raw) :

Pos.Raw

source

@[extern lean_string_isempty]

opaque String.Internal.isEmpty (s : String) :

Bool

source

@[extern lean_string_foldl]

opaque String.Internal.foldl (f : String → Char → String) (init s : String) :

String

source

@[extern lean_string_isprefixof]

opaque String.Internal.isPrefixOf (p s : String) :

Bool

source

@[extern lean_string_any]

opaque String.Internal.any (s : String) (p : Char → Bool) :

Bool

source

@[extern lean_string_contains]

opaque String.Internal.contains (s : String) (c : Char) :

Bool

source

@[extern lean_string_utf8_get]

opaque String.Internal.get (s : String) (p : Pos.Raw) :

Char

source

@[extern lean_string_capitalize]

opaque String.Internal.capitalize (s : String) :

String

source

@[extern lean_string_utf8_at_end]

opaque String.Internal.atEnd :

String → Pos.Raw → Bool

source

@[extern lean_string_nextwhile]

opaque String.Internal.nextWhile (s : String) (p : Char → Bool) (i : Pos.Raw) :

Pos.Raw

source

@[extern lean_string_trim]

opaque String.Internal.trim (s : String) :

String

source

@[extern lean_string_intercalate]

opaque String.Internal.intercalate (s : String) :

List String → String

source

@[extern lean_string_front]

opaque String.Internal.front (s : String) :

Char

source

@[extern lean_string_drop]

opaque String.Internal.drop (s : String) (n : Nat) :

String

source

@[extern lean_string_dropright]

opaque String.Internal.dropRight (s : String) (n : Nat) :

String

source

@[extern lean_string_get_byte_fast]

opaque String.Internal.getUTF8Byte (s : String) (n : Nat) (h : n < s.utf8ByteSize) :

UInt8

source

@[extern lean_string_mk]

def String.ofList (data : List Char) :

String

Creates a string that contains the characters in a list, in order.

Examples:

['L', '∃', '∀', 'N'].asString = "L∃∀N"
[].asString = ""
['a', 'a', 'a'].asString = "aaa"

Equations

String.ofList data = { bytes := data.utf8Encode, isValidUTF8 := ⋯ }

Instances For

source

@[extern lean_string_mk, deprecated String.ofList (since := "2025-10-30")]

def String.mk (data : List Char) :

String

Equations

String.mk data = { bytes := data.utf8Encode, isValidUTF8 := ⋯ }

Instances For

source

@[inline, deprecated String.ofList (since := "2025-10-30")]

def List.asString (s : List Char) :

String

Creates a string that contains the characters in a list, in order.

Examples:

['L', '∃', '∀', 'N'].asString = "L∃∀N"
[].asString = ""
['a', 'a', 'a'].asString = "aaa"

Equations

s.asString = String.ofList s

Instances For

source

@[extern lean_substring_tostring]

opaque Substring.Raw.Internal.toString :

Raw → String

source

@[extern lean_substring_drop]

opaque Substring.Raw.Internal.drop :

Raw → Nat → Raw

source

@[extern lean_substring_front]

opaque Substring.Raw.Internal.front (s : Raw) :

Char

source

@[extern lean_substring_takewhile]

opaque Substring.Raw.Internal.takeWhile :

Raw → (Char → Bool) → Raw

source

@[extern lean_substring_extract]

opaque Substring.Raw.Internal.extract :

Raw → String.Pos.Raw → String.Pos.Raw → Raw

source

@[extern lean_substring_all]

opaque Substring.Raw.Internal.all (s : Raw) (p : Char → Bool) :

Bool

source

@[extern lean_substring_beq]

opaque Substring.Raw.Internal.beq (ss1 ss2 : Raw) :

Bool

source

@[extern lean_substring_isempty]

opaque Substring.Raw.Internal.isEmpty (ss : Raw) :

Bool

source

@[extern lean_substring_get]

opaque Substring.Raw.Internal.get :

Raw → String.Pos.Raw → Char

source

@[extern lean_substring_prev]

opaque Substring.Raw.Internal.prev :

Raw → String.Pos.Raw → String.Pos.Raw

source

@[extern lean_string_pos_sub]

opaque String.Pos.Raw.Internal.sub :

Raw → Raw → Raw

source

@[extern lean_string_pos_min]

opaque String.Pos.Raw.Internal.min (p₁ p₂ : Raw) :

Raw

source

@[inline]

def Char.toString (c : Char) :

String

Constructs a singleton string that contains only the provided character.

Examples:

'L'.toString = "L"
'"'.toString = "\""

Equations

c.toString = String.singleton c

Instances For