Module MetaProverState_intf.S.Result

module Result: sig .. end

type t

val lemmas : t -> MetaProverState_intf.S.lemma list

Discovered lemmas

val theories : t -> MetaProverState_intf.S.theory list

Detected theories

val axioms : t -> MetaProverState_intf.S.axiom list

Additional axioms

val rewrite : t -> MetaProverState_intf.S.rewrite list

List of term rewrite systems

val pre_rewrite : t -> MetaProverState_intf.S.pre_rewrite list

Pre-processing rules

val print : Format.formatter -> t -> unit