Up – coq » UtilModule Util type 'a pervasives_ref = 'a Stdlib.refval pervasives_ref : 'a -> 'a Stdlib.refval pervasives_compare : 'a -> 'a -> intval (!) : 'a Stdlib.ref -> 'a val (+) : int -> int -> intval (-) : int -> int -> intThis 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 -> boolval is_digit : char -> boolval is_ident_tail : char -> boolval is_blank : char -> boolmodule Empty : sig ... end val subst_command_placeholder : string -> string -> stringSubstitute %s in the first chain by the second chain
val (@) : 'a list -> 'a list -> 'a listval stream_nth : int -> 'a Stdlib.Stream.t -> 'a val stream_njunk : int -> 'a Stdlib.Stream.t -> unitval matrix_transpose : 'a list list -> 'a list listval 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 -> unitval 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_channelOpen 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