package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=66e57ea55275903bef74d5bf36fbe0f1
sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b
doc/coq-core.kernel/Pstring/index.html
Module Pstring
Source
Primitive string
type.
to_string s
converts the primitive string s
into a standard string.
of_string s
converts string s
into a primitive string if its size does not exceed max_length_int
, and returns None
otherwise.
make i c
returns a string of size min i max_length
containing only the character with code c l_and 255
.
get s i
gives the code of the character stored at index i
in s
. When index i
is invalid, the function returns zero.
sub s off len
returns the substring of s
starting at offset off
, and of length len
, when possible. If off
is not a valid offset in s
, the empty string is returned. If off
is a valid offset, the function returns the longest possible suffix of s
that: (1) starts at off
, and (2) does not have more than len
characters.
cat s1 s2
returns the concatenation of s1
and of the longest prefix of s2
such that the sum of their lengths does not exceed max_length
.
compare s1 s2
returns 0
if s1
and s2
are equal, a number less than 0
if s1
is smaller than s2
, and a number greater than 0
if s1
is greater than s2
.
unsafe_of_string s
converts s
into a primitive string without checking whether its size satisfies the length constraint. Callers of this function must ensure that length s <= max_length_int
, which is always the case if s
was obtained via to_string
. NOTE: this function is used in generated code, via compile
.