Module BottomUp.Univ

module Univ: sig .. end

This module is present to allow the user to extend explanations with her own types.

This is largely inspired by this thread

type t

The universal type

type 'a embedding

Conversion between the universal type and 'a

val embed : unit -> 'a embedding

Create a new embedding. Values packed by a given embedding can only be unpacked by the same embedding.

val pack : 'a embedding -> 'a -> t

val unpack : 'a embedding -> t -> 'a option

val compatible : 'a embedding -> t -> bool