Module Prelude_extracted.String

Byte strings

These strings correspond to OCaml native strings, and do not have a particular unicode encoding.

Rather, they should be seen as sequences of bytes, and it is also this way that Imandra considers them.

type t = string
val empty : string
val length_ : t -> int
val length : t -> int

Length of the string, i.e. its number of bytes

val make : Program_prelude_.Int.t -> char -> t

make i c makes a string containing i times the char c

val append : t -> t -> t

String concatenation

val get : string -> int -> char
val concat : t -> t list -> t

concat sep l concatenates strings in l with sep inserted between each element.

  • concat sep [] = ""
  • concat sep [x] = x
  • concat sep [x;y] = x ^ sep ^ y
  • concat sep (x :: tail) = x ^ sep ^ concat sep tail
val prefix : t -> t -> bool

prefix a b returns true iff a is a prefix of b (or if a=b

val suffix : t -> t -> bool

suffix a b returns true iff a is a suffix of b (or if a=b

val contains : t -> t -> bool
val unsafe_sub_ : t -> int -> int -> t
val unsafe_sub : t -> int -> int -> t
val sub : t -> int -> int -> t option

Substring. sub s i len returns the string s[i], s[i+1],…,s[i+len-1].

val of_int : int -> t

String representation of an integer

val unsafe_to_nat : t -> int
val to_nat : t -> int option

Parse a string into a nonnegative number, or return None

val is_nat : t -> bool
val is_int : t -> bool
val unsafe_to_int : t -> int
val to_int : t -> int option