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.mk (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.mk data = { bytes := data.utf8Encode, isValidUTF8 := ⋯ }

Instances For

source
@[inline]
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.mk s

Instances For

source
@[extern lean_substring_tostring]
opaque Substring.Internal.toString :
Substring → String
source
@[extern lean_substring_drop]
opaque Substring.Internal.drop :
Substring → Nat → Substring
source
@[extern lean_substring_front]
opaque Substring.Internal.front (s : Substring) :
Char
source
@[extern lean_substring_takewhile]
opaque Substring.Internal.takeWhile :
Substring → (Char → Bool) → Substring
source
@[extern lean_substring_extract]
opaque Substring.Internal.extract :
Substring → String.Pos.Raw → String.Pos.Raw → Substring
source
@[extern lean_substring_all]
opaque Substring.Internal.all (s : Substring) (p : Char → Bool) :
Bool
source
@[extern lean_substring_beq]
opaque Substring.Internal.beq (ss1 ss2 : Substring) :
Bool
source
@[extern lean_substring_isempty]
opaque Substring.Internal.isEmpty (ss : Substring) :
Bool
source
@[extern lean_substring_get]
opaque Substring.Internal.get :
Substring → String.Pos.Raw → Char
source
@[extern lean_substring_prev]
opaque Substring.Internal.prev :
Substring → 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