package coq

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

Module UtilSource

Sourcetype 'a pervasives_ref = 'a ref
Sourceval pervasives_ref : 'a -> 'a ref
Sourceval pervasives_compare : 'a -> 'a -> int
Sourceval (!) : 'a ref -> 'a
Sourceval (+) : int -> int -> int
Sourceval (-) : int -> int -> int

This module contains numerous utility functions on strings, lists, arrays, etc.

Mapping under pairs

Sourceval on_fst : ('a -> 'b) -> ('a * 'c) -> 'b * 'c
Sourceval on_snd : ('a -> 'b) -> ('c * 'a) -> 'c * 'b
Sourceval map_pair : ('a -> 'b) -> ('a * 'a) -> 'b * 'b

Mapping under triplets

Sourceval on_pi1 : ('a -> 'b) -> ('a * 'c * 'd) -> 'b * 'c * 'd
Sourceval on_pi2 : ('a -> 'b) -> ('c * 'a * 'd) -> 'c * 'b * 'd
Sourceval on_pi3 : ('a -> 'b) -> ('c * 'd * 'a) -> 'c * 'd * 'b
Projections from triplets
Sourceval pi1 : ('a * 'b * 'c) -> 'a
Sourceval pi2 : ('a * 'b * 'c) -> 'b
Sourceval pi3 : ('a * 'b * 'c) -> 'c
Chars.
Sourceval is_letter : char -> bool
Sourceval is_digit : char -> bool
Sourceval is_ident_tail : char -> bool
Sourceval is_blank : char -> bool
Empty type
Sourcemodule Empty : sig ... end
Strings.
Sourceval subst_command_placeholder : string -> string -> string

Substitute %s in the first chain by the second chain

Lists.
Sourceval (@) : 'a list -> 'a list -> 'a list
Arrays.
Sets.
Sourcemodule Set : module type of CSet
Maps.
Sourcemodule Map : module type of CMap
Streams.
Sourceval stream_nth : int -> 'a Stream.t -> 'a
Sourceval stream_njunk : int -> 'a Stream.t -> unit
Matrices.
Sourceval matrix_transpose : 'a list list -> 'a list list
Functions.
Sourceval identity : 'a -> 'a
Sourceval (%>) : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c

Left-to-right function composition:

f1 %> f2 is fun x -> f2 (f1 x).

f1 %> f2 %> f3 is fun x -> f3 (f2 (f1 x)).

f1 %> f2 %> f3 %> f4 is fun x -> f4 (f3 (f2 (f1 x)))

etc.

Sourceval const : 'a -> 'b -> 'a
Sourceval iterate : ('a -> 'a) -> int -> 'a -> 'a
Sourceval repeat : int -> ('a -> unit) -> 'a -> unit
Sourceval app_opt : ('a -> 'a) option -> 'a -> 'a
Delayed computations.
Sourcetype 'a delayed = unit -> 'a
Sourceval delayed_force : 'a delayed -> 'a
Sourceval try_finally : ('a -> 'b) -> 'a -> ('c -> unit) -> 'c -> 'b

try_finally f x g y applies the main code f to x and returns the result after having applied the finalization code g to y. If the main code raises the exception exn, the finalization code is executed and exn is raised. If the finalization code itself fails, the exception returned is always the one from the finalization code. Credit X.Leroy, D.Remy.

Enriched exceptions
Sourcetype iexn = Exninfo.iexn
  • deprecated please use [Exninfo.iexn]
Sourceval iraise : Exninfo.iexn -> 'a
  • deprecated please use [Exninfo.iraise]
Misc.
Sourcetype ('a, 'b) union = ('a, 'b) CSig.union =
  1. | Inl of 'a
  2. | Inr of 'b
    (*

    Union type

    *)
Sourcemodule Union : sig ... end
Sourceval map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union

Alias for Union.map

Sourcetype 'a until = 'a CSig.until =
  1. | Stop of 'a
  2. | Cont of 'a
    (*

    Used for browsable-until structures.

    *)
Sourcetype ('a, 'b) eq = ('a, 'b) CSig.eq =
  1. | Refl : ('a, 'a) eq
Sourceval sym : ('a, 'b) eq -> ('b, 'a) eq
Sourceval open_utf8_file_in : string -> in_channel

Open an utf-8 encoded file and skip the byte-order mark if any.

Sourceval set_temporary_memory : unit -> ('a -> 'a) * (unit -> 'a)

A trick which can typically be used to store on the fly the computation of values in the "when" clause of a "match" then retrieve the evaluated result in the r.h.s of the clause

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