Building a Preface_specs.Decidable
Build a Preface_specs.DECIDABLE using Preface_specs.Divisible.WITH_DIVIDE_AND_CONQUER and Preface_specs.Decidable.WITH_LOSE_AND_CHOOSE. contramap will be derived using divide and conquer.
Standard method, using the minimal definition of a Divisible to derive its full API.
module Via_divide_and_conquer
(Divisible_req : Preface_specs.Divisible.WITH_DIVIDE_AND_CONQUER)
(Req :
Preface_specs.Decidable.WITH_LOSE_AND_CHOOSE
with type 'a t = 'a Divisible_req.t) :
Preface_specs.DECIDABLE with type 'a t = 'a Req.tBuild a Preface_specs.DECIDABLE using Preface_specs.Decidable.WITH_CONTRAMAP_AND_DIVIDE_AND_CONQUER and Preface_specs.Decidable.WITH_LOSE_AND_CHOOSE.
Standard method, using the minimal definition of a Divisible to derive its full API.
module Via_contramap_and_divide_and_conquer
(Divisible_req :
Preface_specs.Divisible.WITH_CONTRAMAP_AND_DIVIDE_AND_CONQUER)
(Req :
Preface_specs.Decidable.WITH_LOSE_AND_CHOOSE
with type 'a t = 'a Divisible_req.t) :
Preface_specs.DECIDABLE with type 'a t = 'a Req.tProduces a Preface_specs.DECIDABLE from a Preface_specs.DIVISIBLE.
module Over_divisible
(Divisible : Preface_specs.Divisible.CORE)
(Req :
Preface_specs.Decidable.WITH_LOSE_AND_CHOOSE
with type 'a t = 'a Divisible.t) :
Preface_specs.DECIDABLE with type 'a t = 'a Req.tAdvanced way to build an Preface_specs.DECIDABLE, constructing and assembling a component-by-component of Preface_specs.DECIDABLE. (In order to provide your own implementation for some features.)
module Via
(Core : Preface_specs.Decidable.CORE)
(Operation : Preface_specs.Decidable.OPERATION with type 'a t = 'a Core.t)
(Infix : Preface_specs.Decidable.INFIX with type 'a t = 'a Operation.t) :
Preface_specs.DECIDABLE with type 'a t = 'a Infix.tmodule Core_via_divide_and_conquer
(Divisible_req : Preface_specs.Divisible.WITH_DIVIDE_AND_CONQUER)
(Req :
Preface_specs.Decidable.WITH_LOSE_AND_CHOOSE
with type 'a t = 'a Divisible_req.t) :
Preface_specs.Decidable.CORE with type 'a t = 'a Req.tmodule Core_via_contramap_and_divide_and_conquer
(Divisible_req :
Preface_specs.Divisible.WITH_CONTRAMAP_AND_DIVIDE_AND_CONQUER)
(Req :
Preface_specs.Decidable.WITH_LOSE_AND_CHOOSE
with type 'a t = 'a Divisible_req.t) :
Preface_specs.Decidable.CORE with type 'a t = 'a Req.tmodule Operation
(Core : Preface_specs.Decidable.CORE) :
Preface_specs.Decidable.OPERATION with type 'a t = 'a Core.tmodule Infix
(Core : Preface_specs.Decidable.CORE)
(Operation : Preface_specs.Decidable.OPERATION with type 'a t = 'a Core.t) :
Preface_specs.Decidable.INFIX with type 'a t = 'a Operation.t