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

val enable_l : Uid.t list -> 'f t -> 'f t
module Induct : sig ... end
module Method : sig ... end
val set_method : Method.t -> 'f t -> 'f t

Update the proof method

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

val apply_hint : 'f t -> 'f list
val add_apply_hints : 'f list -> 'f t -> 'f t
val map_apply_hints : ('a -> 'b) -> 'a t -> 'b t
val induct_hints : _ t -> Induct.t option
val print : 'f CCFormat.printer -> 'f t CCFormat.printer
val chash : 'f Imandra_util.Chash.hasher -> 'f t Imandra_util.Chash.hasher