Module Imandra_surface.Hints
Verification hints for Imandra
type +'f t
Hints are used by the user to instruct the automatic prover built in Imandra. They are parametrized by the type of function definitions
f
.
val default : _ t
val disable : Uid.t -> 'f t -> 'f t
Disable given function, i.e. insert it into the basis so its definition is opaque from now on
val disable_l : Uid.t list -> 'f t -> 'f t
val enable : Uid.t -> 'f t -> 'f t
Remove function from the basis
module Induct : sig ... end
module Method : sig ... end
val method_ : _ t -> Method.t
val make : Method.t -> 'f t
val auto : _ t
val induct : _ t
val unroll : _ t
val unroll_with : int -> _ t
val set_otf : 'f t -> bool -> 'f t
val otf : _ t -> bool
val basis : _ t -> Imandra_surface.Uid.Set.t
Extract a basis, i.e. a set of functions whose definition is ignored for the current proof