Module Combine.RightSource

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

This functor allows you to use syntax helpers defined for theory B (like StringEq.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