package coq-core

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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.