package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=13a67c0a4559ae22e9765c8fdb88957b16c2b335a2d5f47e4d6d9b4b8b299926
doc/coq-core.lib/Explore/index.html
Module Explore
Source
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.
...
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
).