Preface_make.InvariantBuilding a Preface_specs.Invariant
Build a Preface_specs.INVARIANT using Preface_specs.Invariant.WITH_INVMAP.
Standard method, using the minimal definition of a contravariant functor to derive its full API.
module Via_invmap
(Req : Preface_specs.Invariant.WITH_INVMAP) :
Preface_specs.Invariant.API with type 'a t = 'a Req.tSpecialize a Preface_specs.FUNCTOR into a Preface_specs.INVARIANT.
module From_functor
(F : Preface_specs.Functor.CORE) :
Preface_specs.Invariant.API with type 'a t = 'a F.tSpecialize a Preface_specs.CONTRAVARIANT into a Preface_specs.INVARIANT.
module From_contravariant
(F : Preface_specs.Contravariant.CORE) :
Preface_specs.Invariant.API with type 'a t = 'a F.t