Up – coq » UtilModule Util
type 'a pervasives_ref
= 'a Stdlib.ref
val pervasives_ref : 'a -> 'a Stdlib.ref
val pervasives_compare : 'a -> 'a -> int
val (!) : 'a Stdlib.ref -> 'a
val (+) : int -> int -> int
val (-) : int -> int -> int
This module contains numerous utility functions on strings, lists, arrays, etc.
val on_fst : ('a -> 'b ) -> ('a * 'c ) -> 'b * 'c
val on_snd : ('a -> 'b ) -> ('c * 'a ) -> 'c * 'b
val map_pair : ('a -> 'b ) -> ('a * 'a ) -> 'b * 'b
val on_pi1 : ('a -> 'b ) -> ('a * 'c * 'd ) -> 'b * 'c * 'd
val on_pi2 : ('a -> 'b ) -> ('c * 'a * 'd ) -> 'c * 'b * 'd
val on_pi3 : ('a -> 'b ) -> ('c * 'd * 'a ) -> 'c * 'd * 'b
Projections from tripletsval pi1 : ('a * 'b * 'c ) -> 'a
val pi2 : ('a * 'b * 'c ) -> 'b
val pi3 : ('a * 'b * 'c ) -> 'c
val is_letter : char -> bool
val is_digit : char -> bool
val is_ident_tail : char -> bool
val is_blank : char -> bool
module Empty : sig ... end
val subst_command_placeholder : string -> string -> string
Substitute %s in the first chain by the second chain
val (@) : 'a list -> 'a list -> 'a list
val stream_nth : int -> 'a Stdlib.Stream.t -> 'a
val stream_njunk : int -> 'a Stdlib.Stream.t -> unit
val matrix_transpose : 'a list list -> 'a list list
val identity : 'a -> 'a
val (%>) : ('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.
val const : 'a -> 'b -> 'a
val iterate : ('a -> 'a ) -> int -> 'a -> 'a
val repeat : int -> ('a -> unit) -> 'a -> unit
val app_opt : ('a -> 'a ) option -> 'a -> 'a
type 'a delayed
= unit -> 'a
val delayed_force : 'a delayed -> 'a
type ('a, 'b) union
= ('a , 'b ) CSig.union
=
|
Inl of 'a
|
Inr of 'b
Union type
module Union : sig ... end
val map_union : ('a -> 'c ) -> ('b -> 'd ) -> ('a , 'b ) union -> ('c , 'd ) union
Alias for Union.map
type 'a until
= 'a CSig.until
=
|
Stop of 'a
|
Cont of 'a
Used for browsable-until structures.
type ('a, 'b) eq
= ('a , 'b ) CSig.eq
=
val sym : ('a , 'b ) eq -> ('b , 'a ) eq
val open_utf8_file_in : string -> Stdlib.in_channel
Open an utf-8 encoded file and skip the byte-order mark if any.
val 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