package rocq-runtime
Install
Dune Dependency
Authors
Maintainers
Sources
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/rocq-runtime.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
.