package coq-core

  1. Overview
  2. Docs
package coq-core
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.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct