Documentation

Init.Data.String.Bootstrap

source
@[implicit_reducible]
instance String.instOfNatRaw :
OfNat Pos.Raw 0
source
@[implicit_reducible]
instance String.instInhabited :
Inhabited String
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"
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:

    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, deprecated String.ofList (since := "2025-10-30")]
      def String.mk (data : List Char) :
      String
      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:

        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:

          Instances For