package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

Authors

Maintainers

Sources

coq-8.20.0.tar.gz
md5=66e57ea55275903bef74d5bf36fbe0f1
sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b

doc/coq-core.kernel/Pstring/index.html

Module PstringSource

Primitive string type.

Sourcetype t = private string
Sourcetype char63 = Uint63.t
Sourceval max_length_int : int
Sourceval max_length : Uint63.t
Sourceval to_string : t -> string

to_string s converts the primitive string s into a standard string.

Sourceval of_string : string -> t option

of_string s converts string s into a primitive string if its size does not exceed max_length_int, and returns None otherwise.

Sourceval make : Uint63.t -> char63 -> t

make i c returns a string of size min i max_length containing only the character with code c l_and 255.

Sourceval length : t -> Uint63.t

length s gives the length of string s.

Sourceval get : t -> Uint63.t -> char63

get s i gives the code of the character stored at index i in s. When index i is invalid, the function returns zero.

Sourceval sub : t -> Uint63.t -> Uint63.t -> t

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.

Sourceval cat : t -> t -> t

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.

Sourceval compare : t -> t -> int

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.

Sourceval equal : t -> t -> bool

equal s1 s2 indicates whether s1 and s2 are equal.

Sourceval hash : t -> int

hash s gives a hash of s, with the same value as Hashtbl.hash s.

Sourceval unsafe_of_string : string -> t

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.

Sourceval compile : t -> string

compile s outputs an OCaml expression producing primitive string s.

OCaml

Innovation. Community. Security.