/usr/lib/coq/user-contrib/AAC_tactics/search_monad.mli is in libaac-tactics-ocaml-dev 8.6.1-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 | (***************************************************************************)
(* This is part of aac_tactics, it is distributed under the terms of the *)
(* GNU Lesser General Public License version 3 *)
(* (see file LICENSE for more details) *)
(* *)
(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *)
(***************************************************************************)
(** Search monad that allows to express non-deterministic algorithms
in a legible maner, or programs that solve combinatorial problems.
@see <http://spivey.oriel.ox.ac.uk/mike/search-jfp.pdf> the
inspiration of this module
*)
(** A data type that represent a collection of ['a] *)
type 'a m
(** {2 Monadic operations} *)
(** bind and return *)
val ( >> ) : 'a m -> ('a -> 'b m) -> 'b m
val return : 'a -> 'a m
(** non-deterministic choice *)
val ( >>| ) : 'a m -> 'a m -> 'a m
(** failure *)
val fail : unit -> 'a m
(** folding through the collection *)
val fold : ('a -> 'b -> 'b) -> 'a m -> 'b -> 'b
(** {2 Derived facilities } *)
val sprint : ('a -> string) -> 'a m -> string
val count : 'a m -> int
val choose : 'a m -> 'a option
val to_list : 'a m -> 'a list
val sort : ('a -> 'a -> int) -> 'a m -> 'a m
val is_empty: 'a m -> bool
val filter : ('a -> bool) -> 'a m -> 'a m
|