package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
Search strategies.
...

A search problem implements the following signature SearchProblem. state is the type of states of the search tree. branching is the branching function; if branching s returns an empty list, then search from s is aborted; successors of s are recursively searched in the order they appear in the list. success determines whether a given state is a success.

pp is a pretty-printer for states used in debugging versions of the search functions.

module type SearchProblem = sig ... end
...

Functor Make returns some search functions given a search problem. Search functions raise Not_found if no success is found. States are always visited in the order they appear in the output of branching (whatever the search method is). Debugging versions of the search functions print the position of the visited state together with the state it-self (using S.pp).

module Make (S : SearchProblem) : sig ... end
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