Module Combine.LeftSource

Lifts a Formula from the combined theory back to theory A.

This functor allows you to use syntax helpers defined for theory A (like VersionLeq.Syntax) within the context of the combined BDD.

Parameters

module F : Formula with type 'kind desc = 'kind t

Signature

type t = F.t
val not : t -> t
val and_ : t -> t -> t
val or_ : t -> t -> t