Module type Expr_intf.S

module type S = sig .. end

Signature of formulas that parametrises the Mcsat Solver Module.

type proof 

An abstract type for proofs

module Term: sig .. end
module Formula: sig .. end