Module `Util`Source

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.

Sourcemodule String = CString

Sourceval subst_command_placeholder : string -> string -> string

Substitute %s in the first chain by the second chain

Lists.

Sourcemodule List : module type of CList

Sourceval (@) : 'a list -> 'a list -> 'a list

Arrays.

Sourcemodule Array : CArray.ExtS

Sets.

Sourcemodule Set : module type of CSet

Maps.

Sourcemodule Map : module type of CMap

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 =

| Inl of 'a
| 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 =

| Stop of 'a
| Cont of 'a
(*
Used for browsable-until structures.
*)

Sourcetype ('a, 'b) eq = ('a, 'b) CSig.eq =

| 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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.lib/Util/index.html

Module `Util`Source

Projections from triplets

Chars.

Empty type

Strings.

Lists.

Arrays.

Sets.

Maps.

Matrices.

Functions.

Delayed computations.

Enriched exceptions

Misc.

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.lib/Util/index.html

Module UtilSource

Projections from triplets

Chars.

Empty type

Strings.

Lists.

Arrays.

Sets.

Maps.

Matrices.

Functions.

Delayed computations.

Enriched exceptions

Misc.

Module `Util`Source