Module MetaProverState

module MetaProverState: sig .. end

Meta Prover for zipperposition

type 'a or_error = [ `Error of string | `Ok of 'a ]

module type S = MetaProverState_intf.S

module Make: functor (E : Env.S) -> S  with module E = E

Interface to `Env`

val key : (module MetaProverState.S) Flex_state.key

val get_env : (module Env.S) -> (module MetaProverState.S)

get_env (module Env) returns the meta-prover saved in Env, assuming the extension has been loaded in Env.
Raises Not_found if the extension was not loaded already.

val extension : Extensions.t

Prover extension